# HG changeset patch
# User haftmann
# Date 1486850015 -3600
# Node ID 49c537d8789646d24c8dfcb7b84353b6b72d9066
# Parent  8c32ce2a01c6de248fadfd7b6f1ce76f0c54f2a0
implicit eta contraction for preprocessed terms avoids unintended implicit eta expansion

diff -r 8c32ce2a01c6 -r 49c537d87896 src/Tools/Code/code_preproc.ML
--- 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)