diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Mar 01 19:55:01 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Mar 01 22:46:31 2014 +0100
@@ -440,7 +440,8 @@
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
-    val (syms, pos) = Syntax.read_token str;
+    val {text, pos, ...} = Syntax.read_token_source str;
+    val syms = Symbol_Pos.explode (text, pos);
     val ast =
       parse_asts ctxt true root (syms, pos)
       |> uncurry (report_result ctxt pos)
@@ -749,8 +750,8 @@
 
 in
 
-val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.language_sort;
-val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.language_type;
+val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false);
+val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false);
 
 fun unparse_term ctxt =
   let
@@ -760,7 +761,7 @@
   in
     unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
-      Markup.language_term ctxt
+      (Markup.language_term false) ctxt
   end;
 
 end;