src/HOL/Decision_Procs/langford.ML

   (case Thm.term_of ct of
     \<^Const>\<open>HOL.conj for _ _\<close> => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
   | _ => [ct]);
 
 val list_conj =
-  foldr1 (fn (A, B) => \<^let>\<open>A = A and B = B in cterm \<open>A \<and> B\<close>\<close>);
+  foldr1 (fn (A, B) => \<^instantiate>\<open>A and B in cterm \<open>A \<and> B\<close>\<close>);
 
 fun mk_conj_tab th =
   let
     fun h acc th =
       (case Thm.prop_of th of

             in
               case ndx of
                 [] => NONE
               | _ =>
                 conj_aci_rule
-                  \<^let>\<open>A = p and B = \<open>list_conj (ndx @ dx)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
+                  \<^instantiate>\<open>A = p and B = \<open>list_conj (ndx @ dx)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
                 |> Thm.abstract_rule xn x
                 |> Drule.arg_cong_rule e
                 |> Conv.fconv_rule
                   (Conv.arg_conv
                     (Simplifier.rewrite
                       (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
                 |> SOME
             end
         | _ =>
             conj_aci_rule
-              \<^let>\<open>A = p and B = \<open>list_conj (eqs @ neqs)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
+              \<^instantiate>\<open>A = p and B = \<open>list_conj (eqs @ neqs)\<close> in cterm \<open>Trueprop A \<equiv> Trueprop B\<close>\<close>
             |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
             |> Conv.fconv_rule
                 (Conv.arg_conv
                   (Simplifier.rewrite
                     (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))