diff -r 24d70f4e690d -r aad9f3cfa1d9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 15 15:35:01 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 15 15:40:35 2010 +0200
@@ -1978,7 +1978,7 @@
     val t = Thm.term_of ct;
     val dummy = @{cprop True};
   in case try HOLogic.dest_Trueprop t
-   of SOME t' => if Code_Runtime.eval NONE
+   of SOME t' => if Code_Runtime.value NONE
          (Eval_Method.get, Eval_Method.put, "Eval_Method.put") (K I) thy t' [] 
        then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
        else dummy