# HG changeset patch
# User wenzelm
# Date 1546527348 -3600
# Node ID 015f43ee4bb7fdf24cf8f54a99ca58c09c2c94bf
# Parent  cfac69e7b962393325bccf4946edca278b11c45f
tuned;

diff -r cfac69e7b962 -r 015f43ee4bb7 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Thu Jan 03 15:55:36 2019 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Thu Jan 03 15:55:48 2019 +0100
@@ -297,9 +297,7 @@
   | eta_abs t = t;
 
 val eta_contract = Config.declare_option_bool ("eta_contract", \<^here>);
-
-fun eta_contr ctxt tm =
-  if Config.get ctxt eta_contract then eta_abs tm else tm;
+fun eta_contr ctxt = Config.get ctxt eta_contract ? eta_abs;
 
 
 (* abstraction *)