merged

--- a/src/Tools/Code/code_preproc.ML	Tue Oct 26 12:21:45 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Oct 26 12:19:31 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;