--- a/src/ZF/Tools/primrec_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/primrec_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -203,18 +203,12 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
+structure P = OuterParse and K = OuterKeyword;
-val primrecP =
+val _ =
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
- (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
-
-val _ = OuterSyntax.add_parsers [primrecP];
+ (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)
+ >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
end;
-end;
-
-