Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
decomp_simp: compare terms, not cterms;
authorwenzelm
Fri, 01 Jul 2005 22:33:59 +0200
changeset 16665 b75568de32c6
parent 16664 7b2e29dcd349
child 16666 9a987b59ecab
decomp_simp: compare terms, not cterms;
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle