more informative check: dummies are always allowed parse_term and should not lead to rejection here;

--- 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