# HG changeset patch
# User wenzelm
# Date 1120250039 -7200
# Node ID b75568de32c60560161df24fd26bb565a896e001
# Parent  7b2e29dcd3496adfbdcdae3a7fbfd7a49415e4fe
decomp_simp: compare terms, not cterms;

diff -r 7b2e29dcd349 -r b75568de32c6 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Jul 01 22:29:19 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Jul 01 22:33:59 2005 +0200
@@ -435,7 +435,7 @@
     val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs));
-    val elhs = if elhs = lhs then lhs else elhs;  (*share identical copies*)
+    val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
     val erhs = Pattern.eta_contract (term_of rhs);
     val perm =
       var_perm (term_of elhs, erhs) andalso