# HG changeset patch
# User wenzelm
# Date 877105154 -7200
# Node ID 787d2659ce4ab8ecdd8b5415546a061281e437f8
# Parent  27c63b757af5171e3b94db8af46acc5477166204
no longer tries bogus eta-contract involving aprops;

diff -r 27c63b757af5 -r 787d2659ce4a src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri Oct 17 18:14:48 1997 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Fri Oct 17 18:19:14 1997 +0200
@@ -145,19 +145,23 @@
       subst_bounds (map (mark_bound o #1) rev_new_vars, body))
   end;
 
+
 (*do (partial) eta-contraction before printing*)
 
 val eta_contract = ref true;
 
 fun eta_contr tm =
   let
+    fun is_aprop (Const ("_aprop", _)) = true
+      | is_aprop _ = false;
+
     fun eta_abs (Abs (a, T, t)) =
           (case eta_abs t of
             t' as f $ u =>
               (case eta_abs u of
                 Bound 0 =>
-                  if not (0 mem loose_bnos f) then incr_boundvars ~1 f
-                  else Abs (a, T, t')
+                  if 0 mem loose_bnos f orelse is_aprop f then Abs (a, T, t')
+                  else  incr_boundvars ~1 f
               | _ => Abs (a, T, t'))
           | t' => Abs (a, T, t'))
       | eta_abs t = t;