eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);

--- a/src/Pure/raw_simplifier.ML	Tue Nov 08 11:56:41 2011 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Nov 08 12:03:51 2011 +0100
@@ -456,7 +456,6 @@
     val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
-    val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
     val erhs = Envir.eta_contract (term_of rhs);
     val perm =
       var_perm (term_of elhs, erhs) andalso