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;