changeset 30589 | cbe27c4ef417 |
parent 30588 | 05f81bbb2614 |
child 30590 | 1d9c9fcf8513 |
--- a/src/Pure/ML/ml_context.ML Thu Mar 19 15:22:53 2009 +0100 +++ b/src/Pure/ML/ml_context.ML Thu Mar 19 15:44:14 2009 +0100 @@ -210,7 +210,8 @@ val lex = #1 (OuterKeyword.get_lexicons ()); fun no_decl _ = ("", ""); - fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state) + fun expand (Antiquote.Text ss) state = + (K ("", Symbol.escape (Symbol_Pos.content ss)), state) | expand (Antiquote.Antiq x) (scope, background) = let val context = Stack.top scope;