src/HOL/Tools/split_rule.ML

--- a/src/HOL/Tools/split_rule.ML	Fri May 28 13:37:28 2010 +0200
+++ b/src/HOL/Tools/split_rule.ML	Fri May 28 13:37:29 2010 +0200
@@ -108,7 +108,7 @@
 
 
 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;