diff -r 1986f18c4940 -r 9cc1ba3c5706 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu Sep 16 16:51:34 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu Sep 16 16:51:34 2010 +0200
@@ -84,7 +84,8 @@
 (* evaluation with freezed code context *)
 
 fun static_eval_conv thy some_ss consts = no_frees_conv
-  (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
+  (Code_Thingol.static_eval_conv_simple thy consts
+    (fn program => fn thy => rewrite_modulo thy some_ss program));
 
 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;