src/HOLCF/fixrec_package.ML
changeset 22101 6d13239d5f52
parent 21025 10b0821a4d11
child 22581 0a995d40160a
--- a/src/HOLCF/fixrec_package.ML	Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOLCF/fixrec_package.ML	Fri Jan 19 22:08:08 2007 +0100
@@ -291,7 +291,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val fixrec_eqn = P.opt_thm_name ":" -- P.prop;
+val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop;
 
 val fixrec_strict = P.opt_keyword "permissive" >> not;
 
@@ -304,7 +304,7 @@
     (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
 
 (* fixpat parser *)
-val fixpat_decl = P.opt_thm_name ":" -- Scan.repeat1 P.prop;
+val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
 
 val fixpatP =
   OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl