--- 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