--- a/src/HOL/Nominal/nominal_datatype.ML Wed Feb 24 07:06:39 2010 -0800
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Feb 24 20:37:01 2010 +0100
@@ -2079,7 +2079,7 @@
local structure P = OuterParse and K = OuterKeyword in
val datatype_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
(P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
fun mk_datatype args =