changeset 27353 | 71c4dd53d4cb |
parent 26881 | bb68f50644a9 |
child 27665 | b9e54ba563b3 |
1.1 --- a/src/Pure/Thy/thy_edit.ML Wed Jun 25 14:54:45 2008 +0200 1.2 +++ b/src/Pure/Thy/thy_edit.ML Wed Jun 25 17:38:32 2008 +0200 1.3 @@ -35,7 +35,7 @@ 1.4 1.5 fun token_source pos src = 1.6 Symbol.source true src 1.7 - |> T.source (SOME false) OuterSyntax.get_lexicons pos; 1.8 + |> T.source (SOME false) OuterKeyword.get_lexicons pos; 1.9 1.10 fun parse_tokens pos src = Source.exhaust (token_source pos src); 1.11