src/HOL/Quotient.thy
changeset 37564 a47bb386b238
parent 37493 2377d246a631
child 37593 2505feaf2d70
--- a/src/HOL/Quotient.thy	Mon Jun 28 07:38:39 2010 +0200
+++ b/src/HOL/Quotient.thy	Mon Jun 28 09:48:36 2010 +0200
@@ -768,7 +768,7 @@
   {* lifts theorems to quotient types *}
 
 method_setup lifting_setup =
-  {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
+  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
   {* sets up the three goals for the quotient lifting procedure *}
 
 method_setup regularize =