src/HOL/Prod.ML

   | Some x => EVERY[res_inst_tac[("p",x)] PairE i,
                     REPEAT(hyp_subst_tac i), prune_params_tac]);
 
 end;
 
-claset_ref() := claset() addSaltern ("split_all_tac", split_all_tac);
+(* claset_ref() := claset() addbefore  ("split_all_tac", TRY o split_all_tac);*)
+   claset_ref() := claset() addSaltern ("split_all_tac",       split_all_tac);
 
 (*** lemmas for splitting paired `!!'
 Does not work with simplifier because it also affects premises in
 congrence rules, where is can lead to premises of the form
 !!a b. ... = ?P(a,b)

 by (stac split 1);
 by (Blast_tac 1);
 qed "expand_split";
 
 (* could be done after split_tac has been speeded up significantly:
-simpset_ref() := (simpset() addsplits [expand_split]);
+simpset_ref() := simpset() addsplits [expand_split];
    precompute the constants involved and don't do anything unless
    the current goal contains one of those constants
 *)
 
 goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";