--- a/src/HOL/Tools/Datatype/datatype.ML Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Feb 24 20:37:01 2010 +0100
@@ -731,7 +731,7 @@
in (names, specs) end;
val parse_datatype_decl =
- (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
+ (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix --
(P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;