diff -r a741416574e1 -r d55224947082 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Tue Jan 29 10:19:58 2008 +0100
+++ b/src/HOL/Library/Eval.thy	Tue Jan 29 10:20:00 2008 +0100
@@ -362,12 +362,9 @@
 
 val eval_ref = ref (NONE : (unit -> term) option);
 
-fun eval_invoke thy code ((_, ty), t) deps _ =
-  CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
-
 fun eval_term thy =
   Eval_Aux.mk_term_of
-  #> CodePackage.eval_term thy (eval_invoke thy)
+  #> (fn t => CodePackage.eval_term ("Eval.eval_ref", eval_ref) thy t [])
   #> Code.postprocess_term thy;
 
 val evaluators = [