src/Pure/Syntax/syntax_phases.ML

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -401,7 +401,7 @@
       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) =>