| changeset 17057 | 0934ac31985f |
| parent 16424 | 18a07ad8fea8 |
| child 17224 | a78339014063 |
--- a/src/ZF/Tools/ind_cases.ML Tue Aug 16 13:42:23 2005 +0200 +++ b/src/ZF/Tools/ind_cases.ML Tue Aug 16 13:42:26 2005 +0200 @@ -79,7 +79,7 @@ (* outer syntax *) -local structure P = OuterParse and K = OuterSyntax.Keyword in +local structure P = OuterParse and K = OuterKeyword in val ind_cases = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)