src/HOL/HOL.thy
changeset 51021 1cf4faed8b22
parent 50360 628b37b9e8a2
child 51304 0e71a248cacb
     1.1 --- a/src/HOL/HOL.thy	Tue Feb 05 17:19:13 2013 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Feb 06 17:18:01 2013 +0100
     1.3 @@ -1265,15 +1265,15 @@
     1.4            val fx_g = Simplifier.rewrite ss (Thm.apply cf cx);
     1.5            val (_ $ _ $ g) = prop_of fx_g;
     1.6            val g' = abstract_over (x,g);
     1.7 +          val abs_g'= Abs (n,xT,g');
     1.8          in (if (g aconv g')
     1.9               then
    1.10                  let
    1.11                    val rl =
    1.12                      cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
    1.13                  in SOME (rl OF [fx_g]) end
    1.14 -             else if Term.betapply (f, x) aconv g then NONE (*avoid identity conversion*)
    1.15 +             else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*)
    1.16               else let
    1.17 -                   val abs_g'= Abs (n,xT,g');
    1.18                     val g'x = abs_g'$x;
    1.19                     val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x));
    1.20                     val rl = cterm_instantiate