# HG changeset patch
# User wenzelm
# Date 1434382183 -7200
# Node ID 9b28f446d9c520688ab52cdf20b05a4d9a4826a7
# Parent  bfd9b7302a82289642b861551a18eae533322f81
more informative check: dummies are always allowed parse_term and should not lead to rejection here;

diff -r bfd9b7302a82 -r 9b28f446d9c5 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Jun 15 16:59:27 2015 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Jun 15 17:29:43 2015 +0200
@@ -399,8 +399,9 @@
           val limit = Config.get ctxt Syntax.ambiguity_limit;
 
           (*brute-force disambiguation via type-inference*)
-          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
-            handle exn as ERROR _ => Exn.Exn exn;
+          fun check t =
+            (Syntax.check_term (Proof_Context.allow_dummies ctxt) (constrain t); Exn.Res t)
+              handle exn as ERROR _ => Exn.Exn exn;
 
           val results' =
             if parsed_len > 1 then