--- a/src/HOL/Tools/record.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/record.ML Mon May 17 23:54:15 2010 +0200
@@ -2460,17 +2460,14 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.command "record" "define extensible record" K.thy_decl
- (P.type_args_constrained -- P.binding --
- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
+ Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
+ (Parse.type_args_constrained -- Parse.binding --
+ (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
+ Scan.repeat1 Parse.const_binding)
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
end;
-end;
-
structure Basic_Record: BASIC_RECORD = Record;
open Basic_Record;