src/HOL/HOL.thy
changeset 36945 9bec62c10714
parent 36936 c52d1c130898
child 37264 8b931fb51cc6
     1.1 --- a/src/HOL/HOL.thy	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -1282,12 +1282,12 @@
     1.4               else let
     1.5                     val abs_g'= Abs (n,xT,g');
     1.6                     val g'x = abs_g'$x;
     1.7 -                   val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
     1.8 +                   val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x));
     1.9                     val rl = cterm_instantiate
    1.10                               [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx),
    1.11                                (g_Let_folded, cterm_of thy abs_g')]
    1.12                               @{thm Let_folded};
    1.13 -                 in SOME (rl OF [transitive fx_g g_g'x])
    1.14 +                 in SOME (rl OF [Thm.transitive fx_g g_g'x])
    1.15                   end)
    1.16          end
    1.17      | _ => NONE)