diff -r b643f4d7b9e9 -r c7ba07e3bbe8 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Wed Jun 21 18:09:09 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy	Wed Jun 21 18:14:28 2000 +0200
@@ -6,7 +6,7 @@
 Eta-reduction and relatives.
 *)
 
-Eta = ParRed + Commutation +
+Eta = ParRed +
 consts free :: dB => nat => bool
        decr :: dB => dB
        eta  :: "(dB * dB) set"