# HG changeset patch
# User wenzelm
# Date 921674979 -3600
# Node ID eed1273c9146645a1ed42d5019d6c17406a48d65
# Parent  45bb139e6ceb5f5156a611402d8e71728ce2db2f
local open OuterParse;

diff -r 45bb139e6ceb -r eed1273c9146 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Mar 17 13:49:14 1999 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Wed Mar 17 13:49:39 1999 +0100
@@ -261,17 +261,20 @@
 
 (* outer syntax *)
 
-open OuterParse;
+local open OuterParse in
 
 val primrec_decl =
   Scan.optional ($$$ "(" |-- name --| $$$ ")") "" --
     Scan.repeat1 (opt_thm_name ":" -- term);
 
 val primrecP =
-  OuterSyntax.parser false "primrec" "define primitive recursive functions on datatypes"
+  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes"
     (primrec_decl >> (fn (alt_name, eqns) =>
       Toplevel.theory (#1 o add_primrec alt_name (map (fn ((x, y), z) => ((x, z), y)) eqns))));
 
 val _ = OuterSyntax.add_parsers [primrecP];
 
 end;
+
+
+end;
diff -r 45bb139e6ceb -r eed1273c9146 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Mar 17 13:49:14 1999 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Mar 17 13:49:39 1999 +0100
@@ -883,14 +883,14 @@
 
 (* outer syntax *)
 
-open OuterParse;
+local open OuterParse in
 
 val record_decl =
   type_args -- name -- ($$$ "=" |-- Scan.option (typ --| $$$ "+")
     -- Scan.repeat1 (name -- ($$$ "::" |-- typ)));
 
 val recordP =
-  OuterSyntax.parser false "record" "define extensible record"
+  OuterSyntax.command "record" "define extensible record"
     (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));
 
 val _ = OuterSyntax.add_parsers [recordP];
@@ -898,5 +898,7 @@
 end;
 
 
+end;
+
 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage;
 open BasicRecordPackage;