changeset 69577 | 015f43ee4bb7 |
parent 69575 | f77cc54f6d47 |
child 74442 | f5c5006d142e |
--- 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 *)