src/Tools/Code/code_runtime.ML
changeset 59633 a372513af1e2
parent 59621 291934bac95e
child 59936 b8ffc3dc9e24
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Mar 06 23:44:57 2015 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Mar 06 23:52:14 2015 +0100
     1.3 @@ -172,12 +172,11 @@
     1.4  
     1.5  fun check_holds ctxt evaluator vs_t ct =
     1.6    let
     1.7 -    val thy = Proof_Context.theory_of ctxt;
     1.8      val t = Thm.term_of ct;
     1.9      val _ = if fastype_of t <> propT
    1.10 -      then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
    1.11 +      then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
    1.12        else ();
    1.13 -    val iff = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    1.14 +    val iff = Thm.cterm_of ctxt (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
    1.15      val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
    1.16       of SOME Holds => true
    1.17        | _ => false;