--- a/src/HOL/Tools/code_evaluation.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Tools/code_evaluation.ML Fri Mar 21 20:33:56 2014 +0100
@@ -193,7 +193,7 @@
val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
val t = Thm.term_of ct;
val T = fastype_of t;
- val mk_eq = Thm.mk_binop (cert (Const ("==", T --> T --> propT)));
+ val mk_eq = Thm.mk_binop (cert (Const (@{const_name Pure.eq}, T --> T --> propT)));
in case value ctxt t
of NONE => Thm.reflexive ct
| SOME t' => conv ctxt (mk_eq ct (cert t')) RS @{thm eq_eq_TrueD}
@@ -206,9 +206,9 @@
fun static_conv ctxt consts Ts =
let
- val eqs = "==" :: @{const_name HOL.eq} ::
+ val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
- (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*)
+ (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
val value = static_value ctxt consts Ts;
val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
in