--- a/Quot/QuotMain.thy	Tue Dec 08 04:14:02 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 04:21:14 2009 +0100
@@ -1074,7 +1074,7 @@
   end)  
 *}
 
-section {* General shape of the lifting procedure *}
+section {* General Shape of the Lifting Procedure *}
 
 (* - A is the original raw theorem          *)
 (* - B is the regularized theorem           *)
@@ -1127,7 +1127,7 @@
 *}
 
 ML {*
-(* leaves three subgoales to be proved *)
+(* the tactic leaves three subgoals to be proved *)
 fun procedure_tac ctxt rthm =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac ctxt
@@ -1142,8 +1142,9 @@
     end)
 *}
 
+(* automatic proofs *)
 ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
 
 fun WARN (tac, msg) i st =
  case Seq.pull ((SOLVES' tac) i st) of