diff --git a/Ivor/TT.lhs b/Ivor/TT.lhs
index 9544f45..491da22 100644
--- a/Ivor/TT.lhs
+++ b/Ivor/TT.lhs
@@ -884,7 +884,7 @@ Convert an internal tactic into a publicly available tactic.
 > -- by unification and solves them (with 'solve').
 > -- See 'refineWith' and 'basicRefine' for slight variations.
 > refine :: IsTerm a => a -> Tactic
-> refine tm = basicRefine tm >=> trySolve
+> refine tm = basicRefine tm >-> keepSolving
 
 > -- | Solve a goal by applying a function.
 > -- If the term given has arguments, this will create a subgoal for each.
@@ -941,8 +941,10 @@ Convert an internal tactic into a publicly available tactic.
 
 > -- | Attach a solution to a goal.
 > fill :: IsTerm a => a -> Tactic
-> fill guess = do rawguess <- raw guess
->                 runTac (Tactics.fill rawguess)
+> fill guess = fill' guess >-> keepSolving
+
+> fill' guess = do rawguess <- raw guess
+>                  runTac (Tactics.fill rawguess)
 
 > -- | Remove a solution from a goal.
 > abandon :: Tactic
@@ -1099,7 +1101,7 @@ FIXME: Choose a sensible name here
 > -- | Apply an eliminator. 
 > by :: IsTerm a => a -- ^ An elimination rule applied to a target.
 >        -> Tactic
-> by rule = by' rule >=> attack
+> by rule = (by' rule >=> attack) >=> keepSolving
 
 > by' rule = do rawrule <- raw rule
 >               runTac (Tactics.by rawrule)
@@ -1107,7 +1109,7 @@ FIXME: Choose a sensible name here
 > -- | Apply the appropriate induction rule to the term.
 > induction :: IsTerm a => a -- ^ target of the elimination
 >                -> Tactic
-> induction tm = induction' tm >=> attack
+> induction tm = (induction' tm >=> attack) >=> keepSolving
 
 > induction' tm = do rawtm <- raw tm
 >                    runTac (Tactics.casetac True rawtm)
@@ -1116,7 +1118,7 @@ FIXME: Choose a sensible name here
 > -- Like 'induction', but no induction hypotheses generated.
 > cases :: IsTerm a => a -- ^ target of the case analysis
 >                -> Tactic
-> cases tm = cases' tm >=> attack
+> cases tm = (cases' tm >=> attack) >=> keepSolving
 > cases' tm = do rawtm <- raw tm
 >                runTac (Tactics.casetac False rawtm)
 
diff --git a/TODO b/TODO
index fb0c162..60c50fa 100644
--- a/TODO
+++ b/TODO
@@ -2,10 +2,8 @@ Short term things to do:
 
 * Current naive proof state representation is far too slow. Come up
   with something better.
-* API shouldn't really need to require use of attack/solve except in
-  specialised cases (e.g. fine control over refinement). Change it so
-  that shell and api are more or less consistent.
 * Keep track of level in proof state.
+* Keep track of binding level in context, and check at point of use.
 * Allow dump of global context to disk, for fast reloading.
 * Syntax for equality.
 * Elimination with a motive.
diff --git a/papers/ivor/corett.tex b/papers/ivor/corett.tex
index 56d973e..e3c51cb 100644
--- a/papers/ivor/corett.tex
+++ b/papers/ivor/corett.tex
@@ -8,7 +8,8 @@ \subsection{The Core Calculus}
 The core type theory of \Ivor{} is a strongly normalising dependent
 type theory with inductive families~\cite{dybjer94}, similar to Luo's
 UTT~\cite{luo94} or the Calculus of Inductive Constructions in
-\Coq{}~\cite{coq-manual}. This language, which I call $\source$, is an
+\Coq{}~\cite{coq-manual}. 
+This language, which I call $\source$, is an
 enriched lambda calculus, with the usual properties of subject
 reduction, Church Rosser, and uniqueness of types up to
 conversion. The strong normalisation property (i.e. that evaluation
@@ -295,3 +296,4 @@ \subsection{Hole Manipulation}
 \end{array}
 }
 
+
diff --git a/papers/ivor/examples.tex b/papers/ivor/examples.tex
index d69534e..5be0a23 100644
--- a/papers/ivor/examples.tex
+++ b/papers/ivor/examples.tex
@@ -1,4 +1,5 @@
-\section{First Order Logic Theorem Prover}
+\section{A First Order Logic Theorem Prover}
 
 \section{\Funl{}, a Functional Language with a Built-in Theorem Prover}
 
+
diff --git a/papers/ivor/tactics.tex b/papers/ivor/tactics.tex
index 7e6c8df..262005f 100644
--- a/papers/ivor/tactics.tex
+++ b/papers/ivor/tactics.tex
@@ -130,17 +130,18 @@ \subsection{Tactic Combinators}
 
 \subsubsection{Sequencing Tactics}
 
-\hdecl{(>->) :: Tactic -> Tactic -> Tactic}
-
-\hdecl{(>=>) :: Tactic -> Tactic -> Tactic}
-
-\hdecl{(>+>) :: Tactic -> Tactic -> Tactic}
+\begin{verbatim}
+(>->) :: Tactic -> Tactic -> Tactic
+(>=>) :: Tactic -> Tactic -> Tactic
+(>+>) :: Tactic -> Tactic -> Tactic
+\end{verbatim}
 
 \subsubsection{Handling Failure}
 
-\hdecl{try :: Tactic -> Tactic -> Tactic -> Tactic}
-
+\begin{verbatim}
+try :: Tactic -> Tactic -> Tactic -> Tactic
+\end{verbatim}
 
 \subsection{The Shell}
 
-\subsection{Extending and Embedding}
\ No newline at end of file
+\subsection{Extending and Embedding}