# HG changeset patch
# User haftmann
# Date 1206010874 -3600
# Node ID 7f50b708376cf39e87e29fe52c4e64b793a57ed0
# Parent  d5125a62f8397c7587adb863e5294e64b7bf47fe
tuned

diff -r d5125a62f839 -r 7f50b708376c src/HOL/Tools/split_rule.ML
--- 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 =