| changeset 17057 | 0934ac31985f |
| parent 15570 | 8d8c70b41bab |
| child 17370 | 754b7fcff03e |
--- a/src/HOL/Import/import_syntax.ML Tue Aug 16 13:42:23 2005 +0200 +++ b/src/HOL/Import/import_syntax.ML Tue Aug 16 13:42:26 2005 +0200 @@ -30,7 +30,7 @@ type token = OuterSyntax.token -local structure P = OuterParse and K = OuterSyntax.Keyword in +local structure P = OuterParse and K = OuterKeyword in (* Parsers *)