# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260242474 -3600
# Node ID 20b8585ad1e0c1e7d7eb09499f85a18d432fca7d
# Parent  386a6b1a520380bf4cfa3266d926dc1f71cb3d51
tuned

diff -r 386a6b1a5203 -r 20b8585ad1e0 Quot/QuotMain.thy
--- 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