src/HOL/Nominal/nominal_datatype.ML
changeset 35351 7425aece4ee3
parent 35232 f588e1169c8b
child 35402 115a5a95710a
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Feb 24 07:06:39 2010 -0800
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Feb 24 20:37:01 2010 +0100
     1.3 @@ -2079,7 +2079,7 @@
     1.4  local structure P = OuterParse and K = OuterKeyword in
     1.5  
     1.6  val datatype_decl =
     1.7 -  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
     1.8 +  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
     1.9      (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
    1.10  
    1.11  fun mk_datatype args =