src/HOL/IOA/Solve.ML

    "(filter_oseq (%a. a:actions(asig_of(C1))) \
 \                (fst ex),                                                \
 \    %i. fst (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (Fast_tac 1);
+ by (fast_tac (claset() delWrapper "split_all_tac") 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
                 addsplits [expand_if,split_option_case]) 1);

    "(filter_oseq (%a. a:actions(asig_of(C2)))\
 \                (fst ex),                                                \
 \    %i. snd (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (Fast_tac 1);
+ by (fast_tac (claset() delWrapper "split_all_tac") 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
                 addsplits [expand_if,split_option_case]) 1);