diff -r 91af1ef45d68 -r 70dd492a1698 src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Wed Feb 25 15:48:04 1998 +0100
+++ b/src/HOL/IOA/Solve.ML	Wed Feb 25 15:51:24 1998 +0100
@@ -73,7 +73,7 @@
 \    %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,
@@ -93,7 +93,7 @@
 \    %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,