src/HOL/Tools/split_rule.ML

           | mk_tuple _ x = x;
         val newt = ap_split' Us U (Var (v, T'));
         val cterm = Thm.cterm_of (Thm.theory_of_thm rl);
         val (vs', insts) = fold mk_tuple ts (vs, []);
       in
-        (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
+        (Drule.instantiate_normalize ([], [(cterm t, cterm newt)] @ insts) rl, vs')
       end
   | complete_split_rule_var _ x = x;
 
 fun collect_vars (Abs (_, _, t)) = collect_vars t
   | collect_vars t =