src/HOL/Tools/split_rule.ML

     |> Rule_Cases.save rl
   end;
 
 
 fun pair_tac ctxt s =
-  res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
+  res_inst_tac ctxt [(("y", 0), s)] @{thm prod.exhaust}
   THEN' hyp_subst_tac
   THEN' K prune_params_tac;
 
 val split_rule_ss = HOL_basic_ss addsimps [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}];