changeset 28054 | 2b84d34c5d02 |
parent 28012 | 2308843f8b66 |
child 28290 | 4cc2b6046258 |
--- a/src/HOL/Code_Setup.thy Thu Aug 28 22:08:11 2008 +0200 +++ b/src/HOL/Code_Setup.thy Thu Aug 28 22:09:20 2008 +0200 @@ -130,7 +130,7 @@ *} oracle eval_oracle ("term") = {* fn thy => fn t => - if CodeTarget.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy + if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy (HOLogic.dest_Trueprop t) [] then t else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)