# HG changeset patch
# User paulson
# Date 831485679 -7200
# Node ID 7d0fbdc46e8eecb219c2ecf244671d9e7a9d58d1
# Parent  cbea219f5e5aa9b9208fc756223f945d0e8811cc
Now split_all_tac works for i>1 !

diff -r cbea219f5e5a -r 7d0fbdc46e8e src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Tue May 07 09:58:12 1996 +0200
+++ b/src/HOL/Prod.ML	Tue May 07 18:14:39 1996 +0200
@@ -58,10 +58,10 @@
 fun is_pair (_,Type("*",_)) = true
   | is_pair _ = false;
 
-fun find_pair_param t =
-  let val params = Logic.strip_params t
+fun find_pair_param prem =
+  let val params = Logic.strip_params prem
   in if exists is_pair params
-     then let val params = rev(rename_wrt_term t params)
+     then let val params = rev(rename_wrt_term prem params)
                            (*as they are printed*)
           in apsome fst (find_first is_pair params) end
      else None
@@ -69,11 +69,11 @@
 
 in
 
-val split_all_tac = REPEAT o SUBGOAL (fn (t,_) =>
-  case find_pair_param t of
+val split_all_tac = REPEAT o SUBGOAL (fn (prem,i) =>
+  case find_pair_param prem of
     None => no_tac
-  | Some x => EVERY[res_inst_tac[("p",x)] PairE 1,
-                    REPEAT(hyp_subst_tac 1), prune_params_tac]);
+  | Some x => EVERY[res_inst_tac[("p",x)] PairE i,
+                    REPEAT(hyp_subst_tac i), prune_params_tac]);
 
 end;