Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
implicit eta contraction for preprocessed terms avoids unintended implicit eta expansion
authorhaftmann
Sat, 11 Feb 2017 22:53:35 +0100
changeset 65026 49c537d87896
parent 65025 8c32ce2a01c6
child 65027 2b8583507891
implicit eta contraction for preprocessed terms avoids unintended implicit eta expansion
src/Tools/Code/code_preproc.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle