src/Pure/Syntax/syntax_phases.ML

   let
     val (markup, kind, root, constrain) =
       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;
+    val decode = constrain o Term_XML.Decode.term (Proof_Context.consts_of ctxt);
   in
     Syntax.parse_input ctxt decode markup
       (fn (syms, pos) =>
         let
           val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);