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