src/Tools/Code/code_runtime.ML

 
 val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of);
 
 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;
   in
     Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct)