--- a/src/HOL/Tools/Datatype/datatype.ML Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Thu Mar 15 20:07:00 2012 +0100
@@ -788,7 +788,7 @@
val spec_cmd =
Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
- (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
+ (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
>> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
val _ =