--- 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;