decomp_simp: compare terms, not cterms;
authorwenzelm
Fri Jul 01 22:33:59 2005 +0200 (2005-07-01)
changeset 16665b75568de32c6
parent 16664 7b2e29dcd349
child 16666 9a987b59ecab
decomp_simp: compare terms, not cterms;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Jul 01 22:29:19 2005 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Jul 01 22:33:59 2005 +0200
     1.3 @@ -435,7 +435,7 @@
     1.4      val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
     1.5        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     1.6      val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs));
     1.7 -    val elhs = if elhs = lhs then lhs else elhs;  (*share identical copies*)
     1.8 +    val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
     1.9      val erhs = Pattern.eta_contract (term_of rhs);
    1.10      val perm =
    1.11        var_perm (term_of elhs, erhs) andalso