--- a/src/Tools/Code/code_runtime.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML Fri Mar 21 20:33:56 2014 +0100
@@ -163,7 +163,7 @@
val _ = if fastype_of t <> propT
then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
else ();
- val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
+ val iff = Thm.cterm_of thy (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;