src/HOL/Code_Setup.thy
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*)