diff -r 1c7e836872b0 -r d88c47ca4557 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Oct 26 12:16:08 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Oct 26 12:19:22 2010 +0200
@@ -481,7 +481,8 @@
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain false thy consts [t'];
   in
-    evaluator algebra' eqngr' vs' t'
+    t'
+    |> evaluator algebra' eqngr' vs'
     |> postproc (postprocess_term thy o resubst)
   end;