--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Sat Oct 17 21:42:18 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Sat Oct 17 22:31:21 2015 +0200
@@ -800,7 +800,7 @@
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 Parse.triple1 cons));
+ >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Scan.triple1 cons));
val _ =
Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"