diff -r 92c43c96027e -r 4e0b89d886ac Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Fri Jan 15 17:09:36 2010 +0100
+++ b/Quot/QuotMain.thy	Sat Jan 16 02:09:38 2010 +0100
@@ -151,15 +151,15 @@
 section {* Methods / Interface *}
 
 ML {*
-fun mk_method1 tac thm ctxt =
-  SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) 
+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.thm >> (mk_method1 Quotient_Tacs.lift_tac) *}
+  {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
   {* Lifting of theorems to quotient types. *}
 
 method_setup lifting_setup =