--- a/src/ZF/Tools/primrec_package.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML Mon May 17 23:54:15 2010 +0200
@@ -194,12 +194,11 @@
(* outer syntax *)
-structure P = OuterParse and K = OuterKeyword;
-
val _ =
- OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
- (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
- >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
+ Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
+ Keyword.thy_decl
+ (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
+ >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
end;