diff -r 820c64273ce0 -r 5cb44fe9ae8e Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 17:35:04 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 17:39:34 2009 +0100
@@ -148,15 +148,15 @@
 (* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 
-lemmas [quotient_thm] =
+lemmas [quot_thm] =
   fun_quotient prod_quotient
 
-lemmas [quotient_rsp] =
+lemmas [quot_respect] =
   quot_rel_rsp pair_rsp
 
 (* fun_map is not here since equivp is not true *)
 (* TODO: option, ... *)
-lemmas [quotient_equiv] =
+lemmas [quot_equiv] =
   identity_equivp prod_equivp
 
 (* definition of the quotient types *)
@@ -1062,6 +1062,7 @@
     EVERY' [lambda_prs_tac lthy,
             simp_tac (simps thms1),
             simp_tac (simps thms2),
+            lambda_prs_tac lthy,
             TRY o rtac refl]
   end
 *}
@@ -1184,9 +1185,8 @@
                     (clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 
+(* 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)) 
@@ -1196,11 +1196,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 =