diff -r b19373bd7ea8 -r a29aefc88c8d src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 13:44:01 2014 +0100
@@ -222,7 +222,9 @@
 (* decode_term -- transform parse tree into raw term *)
 
 fun decode_const ctxt c =
-  let val (Const (c', _), _) = Proof_Context.check_const_proper ctxt false (c, Position.none)
+  let
+    val (Const (c', _), _) =
+      Proof_Context.check_const ctxt {proper = true, strict = false} dummyT (c, Position.none);
   in c' end;
 
 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result