src/HOL/HOL.thy
changeset 59582 0fbed69ff081
parent 59507 b468e0f8da2a
child 59586 ddf6deaadfe8
     1.1 --- a/src/HOL/HOL.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -1193,14 +1193,14 @@
     1.4  simproc_setup let_simp ("Let x f") = {*
     1.5  let
     1.6    val (f_Let_unfold, x_Let_unfold) =
     1.7 -    let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_unfold}
     1.8 -    in (cterm_of @{theory} f, cterm_of @{theory} x) end
     1.9 +    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
    1.10 +    in (Thm.cterm_of @{theory} f, Thm.cterm_of @{theory} x) end
    1.11    val (f_Let_folded, x_Let_folded) =
    1.12 -    let val [(_ $ (f $ x) $ _)] = prems_of @{thm Let_folded}
    1.13 -    in (cterm_of @{theory} f, cterm_of @{theory} x) end;
    1.14 +    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded}
    1.15 +    in (Thm.cterm_of @{theory} f, Thm.cterm_of @{theory} x) end;
    1.16    val g_Let_folded =
    1.17 -    let val [(_ $ _ $ (g $ _))] = prems_of @{thm Let_folded}
    1.18 -    in cterm_of @{theory} g end;
    1.19 +    let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded}
    1.20 +    in Thm.cterm_of @{theory} g end;
    1.21    fun count_loose (Bound i) k = if i >= k then 1 else 0
    1.22      | count_loose (s $ t) k = count_loose s k + count_loose t k
    1.23      | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
    1.24 @@ -1222,11 +1222,11 @@
    1.25        else
    1.26          let
    1.27            val n = case f of (Abs (x, _, _)) => x | _ => "x";
    1.28 -          val cx = cterm_of thy x;
    1.29 -          val {T = xT, ...} = rep_cterm cx;
    1.30 -          val cf = cterm_of thy f;
    1.31 +          val cx = Thm.cterm_of thy x;
    1.32 +          val {T = xT, ...} = Thm.rep_cterm cx;
    1.33 +          val cf = Thm.cterm_of thy f;
    1.34            val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
    1.35 -          val (_ $ _ $ g) = prop_of fx_g;
    1.36 +          val (_ $ _ $ g) = Thm.prop_of fx_g;
    1.37            val g' = abstract_over (x,g);
    1.38            val abs_g'= Abs (n,xT,g');
    1.39          in (if (g aconv g')
    1.40 @@ -1238,10 +1238,10 @@
    1.41               else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*)
    1.42               else let
    1.43                     val g'x = abs_g'$x;
    1.44 -                   val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x));
    1.45 +                   val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of thy g'x));
    1.46                     val rl = cterm_instantiate
    1.47 -                             [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx),
    1.48 -                              (g_Let_folded, cterm_of thy abs_g')]
    1.49 +                             [(f_Let_folded, Thm.cterm_of thy f), (x_Let_folded, cx),
    1.50 +                              (g_Let_folded, Thm.cterm_of thy abs_g')]
    1.51                               @{thm Let_folded};
    1.52                   in SOME (rl OF [Thm.transitive fx_g g_g'x])
    1.53                   end)