--- a/src/Tools/Code/code_preproc.ML Sat Feb 11 22:53:33 2017 +0100
+++ b/src/Tools/Code/code_preproc.ML Sat Feb 11 22:53:35 2017 +0100
@@ -239,9 +239,10 @@
fun pre_conv ctxt' =
Simplifier.rewrite (put_simpset pre ctxt')
#> trans_conv_rule (Axclass.unoverload_conv ctxt')
+ #> trans_conv_rule (Thm.eta_conversion);
fun post_conv ctxt'' =
Axclass.overload_conv ctxt''
- #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt''))
+ #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt''));
in
fn ctxt' => timed_conv "preprocessing term" pre_conv ctxt'
#> pair (timed_conv "postprocessing term" post_conv)