--- a/src/ZF/Tools/inductive_package.ML Sat Oct 17 21:42:18 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Oct 17 22:31:21 2015 +0200
@@ -579,7 +579,8 @@
(* outer syntax *)
fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
- #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
+ #1 o add_inductive doms (map (fn ((x, y), z) => ((x, z), y)) intrs)
+ (monos, con_defs, type_intrs, type_elims);
val ind_decl =
(@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term --