--- a/src/HOL/Tools/primrec_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -350,15 +350,13 @@
val primrec_decl =
opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
-val primrecP =
+val _ =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
(primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
Toplevel.theory (snd o
(if unchecked then add_primrec_unchecked else add_primrec) alt_name
(map P.triple_swap eqns))));
-val _ = OuterSyntax.add_parsers [primrecP];
-
end;
end;