1.1 --- a/src/HOL/Tools/primrec_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -350,15 +350,13 @@
     1.4  val primrec_decl =
     1.5    opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
     1.6  
     1.7 -val primrecP =
     1.8 +val _ =
     1.9    OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
    1.10      (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
    1.11        Toplevel.theory (snd o
    1.12          (if unchecked then add_primrec_unchecked else add_primrec) alt_name
    1.13            (map P.triple_swap eqns))));
    1.14  
    1.15 -val _ = OuterSyntax.add_parsers [primrecP];
    1.16 -
    1.17  end;
    1.18  
    1.19  end;