tuned

--- a/src/HOL/Tools/split_rule.ML	Thu Mar 20 12:01:13 2008 +0100
+++ b/src/HOL/Tools/split_rule.ML	Thu Mar 20 12:01:14 2008 +0100
@@ -123,6 +123,9 @@
   end;
 
 
+fun pair_tac s =
+  EVERY' [res_inst_tac [("p", s)] @{thm PairE}, hyp_subst_tac, K prune_params_tac];
+
 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
 
 fun split_rule_goal xss rl =