diff -r 34d61938e27a -r f0364f1c0ecf src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Thu Aug 14 19:52:39 2008 +0200 +++ b/src/Pure/ML/ml_context.ML Thu Aug 14 19:52:40 2008 +0200 @@ -124,9 +124,11 @@ fun eval_antiquotes struct_name (txt, pos) opt_ctxt = let - val ants = Antiquote.read (txt, pos); + val syms = SymbolPos.explode (txt, pos); + val ants = Antiquote.read (syms, pos); val ((ml_env, ml_body), opt_ctxt') = - if not (exists Antiquote.is_antiq ants) then (("", Symbol.escape txt), opt_ctxt) + if not (exists Antiquote.is_antiq ants) + then (("", Symbol.escape (SymbolPos.content syms)), opt_ctxt) else let val ctxt =