src/HOL/Tools/primrec_package.ML
changeset 22101 6d13239d5f52
parent 21064 9684dd7c81b5
child 22480 b20bc8029edb
--- a/src/HOL/Tools/primrec_package.ML	Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Fri Jan 19 22:08:08 2007 +0100
@@ -321,7 +321,7 @@
       P.name >> pair false) --| P.$$$ ")")) (false, "");
 
 val primrec_decl =
-  opt_unchecked_name -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+  opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
 
 val primrecP =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl