diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Thu Apr 19 08:45:13 2012 +0200 +++ b/src/Tools/Code/code_simp.ML Thu Apr 19 10:16:51 2012 +0200 @@ -53,7 +53,7 @@ (* evaluation with dynamic code context *) fun dynamic_conv thy = Code_Thingol.dynamic_conv thy - (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program); + (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program); fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE;