diff -r 520a4084d064 -r b029f242d85d Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 17:30:00 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 17:33:51 2009 +0100
@@ -1188,8 +1188,6 @@
 
 (* methods / interface *)
 ML {*
-val rule_spec =  Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm
-
 (* FIXME: if the argument order changes then this can be just one function *)
 fun mk_method1 tac thm ctxt =
   SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) 
@@ -1199,11 +1197,11 @@
 *}
 
 method_setup lifting =
-  {* rule_spec >> (mk_method1 lift_tac) *}
+  {* Attrib.thm >> (mk_method1 lift_tac) *}
   {* Lifting of theorems to quotient types. *}
 
 method_setup lifting_setup =
-  {* rule_spec >> (mk_method1 procedure_tac) *}
+  {* Attrib.thm >> (mk_method1 procedure_tac) *}
   {* Sets up the three goals for the lifting procedure. *}
 
 method_setup regularize =