src/ZF/Tools/primrec_package.ML

     args) thy;
 
 
 (* 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;