tuned;

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