--- 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"