--- a/src/Tools/Code/code_runtime.ML Fri Mar 06 23:44:57 2015 +0100
+++ b/src/Tools/Code/code_runtime.ML Fri Mar 06 23:52:14 2015 +0100
@@ -172,12 +172,11 @@
fun check_holds ctxt evaluator vs_t ct =
let
- val thy = Proof_Context.theory_of ctxt;
val t = Thm.term_of ct;
val _ = if fastype_of t <> propT
- then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
+ then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
else ();
- val iff = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
+ val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
of SOME Holds => true
| _ => false;