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