# HG changeset patch
# User hoelzl
# Date 1360167481 -3600
# Node ID 1cf4faed8b220aa840ab56b825e68bbd5a5b2460
# Parent  242cd1632b0b89a75519e62d0ec8d15aaf1f1b88
check alpha equality after applying beta and eta conversion in let-simproc, otherwise the simplifier may loop

diff -r 242cd1632b0b -r 1cf4faed8b22 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Feb 05 17:19:13 2013 +0100
+++ b/src/HOL/HOL.thy	Wed Feb 06 17:18:01 2013 +0100
@@ -1265,15 +1265,15 @@
           val fx_g = Simplifier.rewrite ss (Thm.apply cf cx);
           val (_ $ _ $ g) = prop_of fx_g;
           val g' = abstract_over (x,g);
+          val abs_g'= Abs (n,xT,g');
         in (if (g aconv g')
              then
                 let
                   val rl =
                     cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
                 in SOME (rl OF [fx_g]) end
-             else if Term.betapply (f, x) aconv g then NONE (*avoid identity conversion*)
+             else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*)
              else let
-                   val abs_g'= Abs (n,xT,g');
                    val g'x = abs_g'$x;
                    val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x));
                    val rl = cterm_instantiate