--- a/src/HOL/Library/Eval_Witness.thy Fri Apr 17 14:29:55 2009 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Fri Apr 17 14:29:56 2009 +0200
@@ -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_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
+ if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
then Thm.cterm_of thy goal
else @{cprop True} (*dummy*)
end