src/Tools/Code/code_simp.ML
changeset 47576 b32aae03e3d6
parent 45620 f2a587696afb
child 48072 ace701efe203
--- 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;