src/Pure/Thy/thy_edit.ML
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