src/HOL/HOL.thy
changeset 60781 2da59cdf531c
parent 60761 a443b08281e2
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/HOL.thy	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -1190,15 +1190,6 @@
     1.4  
     1.5  simproc_setup let_simp ("Let x f") = \<open>
     1.6  let
     1.7 -  val (f_Let_unfold, x_Let_unfold) =
     1.8 -    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
     1.9 -    in apply2 (Thm.cterm_of @{context}) (f, x) end
    1.10 -  val (f_Let_folded, x_Let_folded) =
    1.11 -    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded}
    1.12 -    in apply2 (Thm.cterm_of @{context}) (f, x) end;
    1.13 -  val g_Let_folded =
    1.14 -    let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded}
    1.15 -    in Thm.cterm_of @{context} g end;
    1.16    fun count_loose (Bound i) k = if i >= k then 1 else 0
    1.17      | count_loose (s $ t) k = count_loose s k + count_loose t k
    1.18      | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
    1.19 @@ -1234,7 +1225,7 @@
    1.20                  if g aconv g' then
    1.21                    let
    1.22                      val rl =
    1.23 -                      cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
    1.24 +                      infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
    1.25                    in SOME (rl OF [fx_g]) end
    1.26                  else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
    1.27                  then NONE (*avoid identity conversion*)
    1.28 @@ -1243,10 +1234,10 @@
    1.29                      val g'x = abs_g' $ x;
    1.30                      val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
    1.31                      val rl =
    1.32 -                      @{thm Let_folded} |> cterm_instantiate
    1.33 -                        [(f_Let_folded, Thm.cterm_of ctxt f),
    1.34 -                         (x_Let_folded, cx),
    1.35 -                         (g_Let_folded, Thm.cterm_of ctxt abs_g')];
    1.36 +                      @{thm Let_folded} |> infer_instantiate ctxt
    1.37 +                        [(("f", 0), Thm.cterm_of ctxt f),
    1.38 +                         (("x", 0), cx),
    1.39 +                         (("g", 0), Thm.cterm_of ctxt abs_g')];
    1.40                    in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
    1.41                end
    1.42            | _ => NONE)