--- a/Quot/Examples/IntEx.thy	Tue Dec 08 17:30:00 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 17:33:51 2009 +0100
@@ -141,7 +141,7 @@
 done
 
 lemma "PLUS a b = PLUS a b"
-apply(lifting_setup rule: test1)
+apply(lifting_setup test1)
 apply(regularize)
 apply(injection)
 apply(cleaning)
@@ -203,7 +203,7 @@
 done
 
 lemma "foldl PLUS x [] = x"
-apply(lifting rule: ho_tst)
+apply(lifting ho_tst)
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
@@ -343,7 +343,7 @@
 done
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
-apply(lifting rule: lam_tst4)
+apply(lifting lam_tst4)
 apply(cleaning)
 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric])

--- 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 =