changeset 39401 | 887f4218a39a |
parent 39388 | fdbb2c55ffc2 |
child 39403 | aad9f3cfa1d9 |
--- a/src/HOL/HOL.thy Wed Sep 15 15:11:40 2010 +0200 +++ b/src/HOL/HOL.thy Wed Sep 15 15:31:32 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_Eval.eval NONE + of SOME t' => if Code_Runtime.eval 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