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