# 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)