# HG changeset patch
# User wenzelm
# Date 1320750231 -3600
# Node ID 23e5af70af07d6c6a4cc77d443922a4577db3189
# Parent  69ec395ef6caac449906ea95fc433e0887818a17
eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);

diff -r 69ec395ef6ca -r 23e5af70af07 src/Pure/raw_simplifier.ML
--- 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