src/HOLCF/Tools/fixrec_package.ML
changeset 24867 e5b55d7be9bb
parent 24707 dfeb98f84e93
child 25132 dffe405b090d
     1.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -299,19 +299,17 @@
     1.4  
     1.5  (* this builds a parser for a new keyword, fixrec, whose functionality 
     1.6  is defined by add_fixrec *)
     1.7 -val fixrecP =
     1.8 +val _ =
     1.9    OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
    1.10      (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec));
    1.11  
    1.12  (* fixpat parser *)
    1.13  val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop;
    1.14  
    1.15 -val fixpatP =
    1.16 +val _ =
    1.17    OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
    1.18      (fixpat_decl >> (Toplevel.theory o add_fixpat));
    1.19  
    1.20 -val _ = OuterSyntax.add_parsers [fixrecP, fixpatP];
    1.21 +end;
    1.22  
    1.23 -end; (* local structure *)
    1.24 -
    1.25 -end; (* struct *)
    1.26 +end;