src/Tools/Code/code_runtime.ML
changeset 59621 291934bac95e
parent 59155 a9a5ddfc2aad
child 59633 a372513af1e2
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -177,7 +177,7 @@
     1.4      val _ = if fastype_of t <> propT
     1.5        then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
     1.6        else ();
     1.7 -    val iff = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
     1.8 +    val iff = Thm.global_cterm_of thy (Term.Const (@{const_name Pure.eq}, propT --> propT --> propT));
     1.9      val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t [])
    1.10       of SOME Holds => true
    1.11        | _ => false;