# HG changeset patch
# User nipkow
# Date 816178453 -3600
# Node ID 1fbf9407757c3bd771ce752a22896c071997db19
# Parent  32f6d6920204d7c7fe7aad1939a2581d66a8738d
Set eta_contract to true.

diff -r 32f6d6920204 -r 1fbf9407757c src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri Nov 10 16:19:45 1995 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sun Nov 12 13:14:13 1995 +0100
@@ -147,7 +147,7 @@
 
 (*do (partial) eta-contraction before printing*)
 
-val eta_contract = ref false;
+val eta_contract = ref true;
 
 fun eta_contr tm =
   let