src/Pure/Syntax/syntax_phases.ML

 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
     Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
 
 fun parse_sort ctxt =
-  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
+  Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
     (fn (syms, pos) =>
       parse_tree ctxt "sort" (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode_sort
       |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
       handle ERROR msg => parse_failed ctxt pos msg "sort");
 
 fun parse_typ ctxt =
-  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type
+  Syntax.parse_input ctxt Term_XML.Decode.typ Markup.language_type
     (fn (syms, pos) =>
       parse_tree ctxt "type" (syms, pos)
       |> uncurry (report_result ctxt pos)
       |> decode_typ
       handle ERROR msg => parse_failed ctxt pos msg "type");

       if is_prop
       then (Markup.language_prop, "prop", "prop", Type.constraint propT)
       else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
     val decode = constrain o Term_XML.Decode.term;
   in
-    Syntax.parse_token ctxt decode markup
+    Syntax.parse_input ctxt decode markup
       (fn (syms, pos) =>
         let
           val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
           val parsed_len = length (proper_results results);
 

               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 source = Syntax.read_token str;
+    val source = Syntax.read_input str;
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
     val ast =
       parse_asts ctxt true root (syms, pos)
       |> uncurry (report_result ctxt pos)