src/HOL/Tools/BNF/bnf_fp_n2m.ML

     val rel_xtor_co_inducts_inst =
       let
         val extract =
           case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
         val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
-        val thetas = AList.group (op =)
-          (mutual_cliques ~~ map (apply2 (Thm.cterm_of lthy)) (raw_phis ~~ pre_phis));
-      in
-        map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
+        val thetas =
+          AList.group (op =)
+            (mutual_cliques ~~
+              map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of lthy u)) (raw_phis ~~ pre_phis));
+      in
+        map2 (infer_instantiate lthy o the o AList.lookup (op =) thetas)
         mutual_cliques rel_xtor_co_inducts
       end
 
     val xtor_rel_co_induct =
       mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys

             val (Ps, names_lthy) = names_lthy
               |> mk_Frees "P" (map (fn T => T --> HOLogic.boolT) fpTs);
             fun mk_Grp_id P =
               let val T = domain_type (fastype_of P);
               in mk_Grp (HOLogic.Collect_const T $ P) (HOLogic.id_const T) end;
-            val cts = map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
+            val cts =
+              map (SOME o Thm.cterm_of names_lthy) (map HOLogic.eq_const As @ map mk_Grp_id Ps);
             fun mk_fp_type_copy_thms thm = map (curry op RS thm)
               @{thms type_copy_Abs_o_Rep type_copy_vimage2p_Grp_Rep};
             fun mk_type_copy_thms thm = map (curry op RS thm)
               @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
           in
-            cterm_instantiate_pos cts xtor_rel_co_induct
+            infer_instantiate' names_lthy cts xtor_rel_co_induct
             |> singleton (Proof_Context.export names_lthy lthy)
             |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
                 fp_or_nesting_rel_eqs)
             |> funpow n (fn thm => thm RS spec)
             |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)

           end
       | Greatest_FP =>
           let
             val cts = NONE :: map (SOME o Thm.cterm_of lthy) (map HOLogic.eq_const As);
           in
-            cterm_instantiate_pos cts xtor_rel_co_induct
+            infer_instantiate' lthy cts xtor_rel_co_induct
             |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
                 fp_or_nesting_rel_eqs)
             |> funpow (2 * n) (fn thm => thm RS spec)
             |> Conv.fconv_rule (Object_Logic.atomize lthy)
             |> funpow n (fn thm => thm RS mp)