src/HOL/Library/Eval_Witness.thy

     | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
       Abs (v, check_type T, dest_exs (n - 1) b)
     | 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
 *}