diff -r a389be05c06f -r 09d02e7365c1 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Jun 02 17:47:03 2000 +0200
+++ b/src/HOL/simpdata.ML	Fri Jun 02 17:47:41 2000 +0200
@@ -62,6 +62,10 @@
 by (rtac refl 1);
 qed "meta_eq_to_obj_eq";
 
+Goal "(%s. f s) = f";
+br refl 1;
+qed "eta_contract_eq";
+
 local
 
   fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
@@ -437,6 +441,7 @@
     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,