# HG changeset patch
# User nipkow
# Date 860667681 -7200
# Node ID 8658bf6c1a5b9eea6b601109a1c831977b9be128
# Parent  602cdeabb89b6cc8e628a03f98b3315263d330bf
Mod because of "Turned Addsimps into AddIffs for datatype laws."

diff -r 602cdeabb89b -r 8658bf6c1a5b src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Thu Apr 10 12:20:55 1997 +0200
+++ b/src/HOL/Lambda/Eta.ML	Thu Apr 10 12:21:21 1997 +0200
@@ -154,6 +154,8 @@
 by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppL]) 6 1);
 by (Blast.depth_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_AppR]) 6 1);
 (*23 seconds?*)
+DelIffs dB.distinct;
+Addsimps dB.distinct;
 by (slow_tac (!claset addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
                       addss !simpset) 1);
 qed "square_beta_eta";