diff -r e3bbc2c4c581 -r 20d01210b9b1 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Mon Apr 20 12:27:23 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Mon Apr 20 16:28:13 2009 +0200
@@ -175,8 +175,7 @@
 fun eval_term thy t =
   t 
   |> Eval.mk_term_of (fastype_of t)
-  |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t [])
-  |> Code.postprocess_term thy;
+  |> (fn t => Code_ML.eval_term NONE ("Eval.eval_ref", eval_ref) thy t []);
 
 end;
 *}