src/Pure/Syntax/syntax_phases.ML

               SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
             | NONE => decode_appl ps asts)
           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)
       |> decode [];
     val _ = Context_Position.reports ctxt (! reports);

     |> pretty_ast markup
   end;
 
 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
     val thy = Proof_Context.theory_of ctxt;
     val syn = Proof_Context.syn_of ctxt;
     val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
   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;