# HG changeset patch
# User blanchet
# Date 1514911100 -3600
# Node ID 706b1cf7b76d6edc1fba6e6e04bcb5c8721a665a
# Parent  6afba546f0e5efe34711c3fe9be309a9a3fd0425
compile

diff -r 6afba546f0e5 -r 706b1cf7b76d src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Jan 02 16:40:54 2018 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Jan 02 17:38:20 2018 +0100
@@ -2094,9 +2094,14 @@
 val nominal_datatype = gen_nominal_datatype Old_Datatype.check_specs;
 val nominal_datatype_cmd = gen_nominal_datatype Old_Datatype.read_specs;
 
+val spec_cmd =
+  Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
+  (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
+  >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Scan.triple1 cons));
+
 val _ =
   Outer_Syntax.command @{command_keyword nominal_datatype} "define nominal datatypes"
-    (Parse.and_list1 Old_Datatype.spec_cmd >>
+    (Parse.and_list1 spec_cmd >>
       (Toplevel.theory o nominal_datatype_cmd Old_Datatype_Aux.default_config));
 
 end