src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML

        REPEAT_DETERM_N m o etac ctxt exE THEN' hyp_subst_tac ctxt THEN'
        SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac ctxt refl));
 
 fun mk_disc_eq_case_tac ctxt ct exhaust discs distincts cases =
   HEADGOAL Goal.conjunction_tac THEN
-  ALLGOALS (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+  ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
     (hyp_subst_tac ctxt THEN'
      SELECT_GOAL (unfold_thms_tac ctxt (@{thms not_True_eq_False not_False_eq_True} @ cases @
        ((refl :: discs @ distincts) RL [eqTrueI, eqFalseI]))) THEN'
      resolve_tac ctxt @{thms TrueI True_not_False False_not_True}));
 

         (if k' = k then mk_case_same_ctr_tac ctxt injects
          else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
   end;
 
 fun mk_case_distrib_tac ctxt ct exhaust cases =
-  HEADGOAL (rtac ctxt (cterm_instantiate_pos [SOME ct] exhaust)) THEN
+  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)) THEN
   ALLGOALS (hyp_subst_tac ctxt THEN' SELECT_GOAL (unfold_thms_tac ctxt cases) THEN' rtac ctxt refl);
 
 fun mk_case_cong_tac ctxt uexhaust cases =
   HEADGOAL (rtac ctxt uexhaust THEN'
     EVERY' (maps (fn casex => [dtac ctxt sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));