changeset 34028 | 1e6206763036 |
parent 33889 | 4328de748fb2 |
child 34209 | c7f621786035 |
--- a/src/HOL/HOL.thy Mon Dec 07 14:54:28 2009 +0100 +++ b/src/HOL/HOL.thy Mon Dec 07 16:27:48 2009 +0100 @@ -1971,7 +1971,7 @@ val t = Thm.term_of ct; val dummy = @{cprop True}; in case try HOLogic.dest_Trueprop t - of SOME t' => if Code_ML.eval NONE + of SOME t' => if Code_Eval.eval NONE ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy else dummy