src/ZF/Tools/primrec_package.ML

--- a/src/ZF/Tools/primrec_package.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Sun May 16 00:02:11 2010 +0200
@@ -198,7 +198,7 @@
 
 val _ =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+    (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
       >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
 
 end;