src/HOL/Tools/Datatype/datatype.ML
changeset 46949 94aa7b81bcf6
parent 46909 3c73a121a387
child 46961 5c6955f487e5
--- 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 _ =