| changeset 46947 | b8c7eb0c2f89 |
| parent 46215 | 0da9433f959e |
| child 46949 | 94aa7b81bcf6 |
--- a/src/ZF/Tools/inductive_package.ML Thu Mar 15 17:45:54 2012 +0100 +++ b/src/ZF/Tools/inductive_package.ML Thu Mar 15 19:02:34 2012 +0100 @@ -576,9 +576,6 @@ (* outer syntax *) -val _ = List.app Keyword.keyword - ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"]; - 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);