--- a/src/HOL/Tools/record.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/record.ML Thu Mar 15 20:07:00 2012 +0100
@@ -2313,7 +2313,7 @@
val _ =
Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
(Parse.type_args_constrained -- Parse.binding --
- (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
+ (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
Scan.repeat1 Parse.const_binding)
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));