--- a/src/HOL/Library/Eval_Witness.thy Mon Dec 07 14:54:28 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy Mon Dec 07 16:27:48 2009 +0100
@@ -68,7 +68,7 @@
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
+ if Code_Eval.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
then Thm.cterm_of thy goal
else @{cprop True} (*dummy*)
end