diff -r 6389a8c1268a -r d651b944c67e src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu May 08 21:17:23 2014 +0200
+++ b/src/Tools/Code/code_simp.ML	Fri May 09 08:13:26 2014 +0200
@@ -76,7 +76,7 @@
 (* evaluation with dynamic code context *)
 
 fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
-  (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
+  (fn program => fn _ => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
 
 fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
   THEN' conclude_tac ctxt NONE ctxt;
@@ -96,7 +96,7 @@
 fun static_conv ctxt some_ss consts =
   Code_Thingol.static_conv_simple ctxt consts
     (fn program => let val conv' = rewrite_modulo ctxt some_ss program
-     in fn ctxt' => fn _ => fn _ => conv' ctxt' end);
+     in fn ctxt' => fn _ => conv' ctxt' end);
 
 fun static_tac ctxt some_ss consts =
   let