changeset 17057 | 0934ac31985f |
parent 15705 | b5edb9dcec9a |
child 17261 | 193b84a70ca4 |
--- a/src/ZF/Tools/datatype_package.ML Tue Aug 16 13:42:23 2005 +0200 +++ b/src/ZF/Tools/datatype_package.ML Tue Aug 16 13:42:26 2005 +0200 @@ -418,7 +418,7 @@ (* outer syntax *) -local structure P = OuterParse and K = OuterSyntax.Keyword in +local structure P = OuterParse and K = OuterKeyword in fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) = #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);