diff -r 7e2c8a63a8f8 -r 2da59cdf531c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/HOL.thy	Sat Jul 25 23:41:53 2015 +0200
@@ -1190,15 +1190,6 @@
 
 simproc_setup let_simp ("Let x f") = \<open>
 let
-  val (f_Let_unfold, x_Let_unfold) =
-    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
-    in apply2 (Thm.cterm_of @{context}) (f, x) end
-  val (f_Let_folded, x_Let_folded) =
-    let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded}
-    in apply2 (Thm.cterm_of @{context}) (f, x) end;
-  val g_Let_folded =
-    let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded}
-    in Thm.cterm_of @{context} g end;
   fun count_loose (Bound i) k = if i >= k then 1 else 0
     | count_loose (s $ t) k = count_loose s k + count_loose t k
     | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
@@ -1234,7 +1225,7 @@
                 if g aconv g' then
                   let
                     val rl =
-                      cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
+                      infer_instantiate ctxt [(("f", 0), cf), (("x", 0), cx)] @{thm Let_unfold};
                   in SOME (rl OF [fx_g]) end
                 else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g')
                 then NONE (*avoid identity conversion*)
@@ -1243,10 +1234,10 @@
                     val g'x = abs_g' $ x;
                     val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of ctxt g'x));
                     val rl =
-                      @{thm Let_folded} |> cterm_instantiate
-                        [(f_Let_folded, Thm.cterm_of ctxt f),
-                         (x_Let_folded, cx),
-                         (g_Let_folded, Thm.cterm_of ctxt abs_g')];
+                      @{thm Let_folded} |> infer_instantiate ctxt
+                        [(("f", 0), Thm.cterm_of ctxt f),
+                         (("x", 0), cx),
+                         (("g", 0), Thm.cterm_of ctxt abs_g')];
                   in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
               end
           | _ => NONE)