src/HOL/Nominal/nominal_primrec.ML

--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Jan 19 22:08:08 2007 +0100
@@ -426,7 +426,7 @@
     (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE)));
 
 val primrec_decl =
-  options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+  options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
 
 val primrecP =
   OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal