changeset 17057 | 0934ac31985f |
parent 16855 | 7563d0eb3414 |
child 17314 | 04e21a27c0ad |
--- a/src/ZF/Tools/inductive_package.ML Tue Aug 16 13:42:23 2005 +0200 +++ b/src/ZF/Tools/inductive_package.ML Tue Aug 16 13:42:26 2005 +0200 @@ -596,7 +596,7 @@ (* outer syntax *) -local structure P = OuterParse and K = OuterSyntax.Keyword in +local structure P = OuterParse and K = OuterKeyword in fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) = #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);