# HG changeset patch
# User paulson
# Date 1134579710 -3600
# Node ID fa075b606571f842a4b31e2e4900c7b019648740
# Parent  b1eab0eb7fec101c327d63662eb76753675d81be
deleted redundant (looping!) simprule

diff -r b1eab0eb7fec -r fa075b606571 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Dec 14 16:14:41 2005 +0100
+++ b/src/HOL/simpdata.ML	Wed Dec 14 18:01:50 2005 +0100
@@ -364,7 +364,6 @@
     HOL_basic_ss addsimps
      ([triv_forall_equality, (* prunes params *)
        True_implies_equals, (* prune asms `True' *)
-       eta_contract_eq, (* prunes eta-expansions *)
        if_True, if_False, if_cancel, if_eq_cancel,
        imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,