diff -r b102e1444851 -r 84a38acbf512 Quot/Quotient.thy
--- a/Quot/Quotient.thy	Mon Feb 15 10:11:26 2010 +0100
+++ b/Quot/Quotient.thy	Mon Feb 15 10:25:17 2010 +0100
@@ -764,33 +764,24 @@
 
 section {* Methods / Interface *}
 
-(* TODO inline *)
-ML {*
-fun mk_method1 tac thms ctxt =
-  SIMPLE_METHOD (HEADGOAL (tac ctxt thms))
-
-fun mk_method2 tac ctxt =
-  SIMPLE_METHOD (HEADGOAL (tac ctxt))
-*}
-
 method_setup lifting =
-  {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
+  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
   {* lifts theorems to quotient types *}
 
 method_setup lifting_setup =
-  {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
+  {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
   {* sets up the three goals for the quotient lifting procedure *}
 
 method_setup regularize =
-  {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
   {* proves the regularization goals from the quotient lifting procedure *}
 
 method_setup injection =
-  {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
   {* proves the rep/abs injection goals from the quotient lifting procedure *}
 
 method_setup cleaning =
-  {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
   {* proves the cleaning goals from the quotient lifting procedure *}
 
 attribute_setup quot_lifted =