src/HOLCF/Tools/fixrec_package.ML
changeset 24867 e5b55d7be9bb
parent 24707 dfeb98f84e93
child 25132 dffe405b090d
--- a/src/HOLCF/Tools/fixrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -299,19 +299,17 @@
 
 (* this builds a parser for a new keyword, fixrec, whose functionality 
 is defined by add_fixrec *)
-val fixrecP =
+val _ =
   OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
     (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
 
 (* fixpat parser *)
 val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
 
-val fixpatP =
+val _ =
   OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
     (fixpat_decl >> (Toplevel.theory o add_fixpat));
 
-val _ = OuterSyntax.add_parsers [fixrecP, fixpatP];
+end;
 
-end; (* local structure *)
-
-end; (* struct *)
+end;