--- a/Quot/QuotMain.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 17:30:00 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 *)
@@ -1063,6 +1063,7 @@
     EVERY' [lambda_prs_tac lthy,
             simp_tac (simps thms1),
             simp_tac (simps thms2),
+            lambda_prs_tac lthy,
             TRY o rtac refl]
   end
 *}
@@ -1185,6 +1186,7 @@
                     (clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 
+(* methods / interface *)
 ML {*
 val rule_spec =  Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thm