src/HOL/Tools/Quotient/quotient_def.ML

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun May 16 00:02:11 2010 +0200
@@ -99,7 +99,7 @@
 
 val quotdef_parser =
   Scan.optional quotdef_decl (NONE, NoSyn) -- 
-    P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
+    P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
 end
 
 val _ =