diff -r 2c109cd2fdd0 -r d22110ddd0af src/HOL/IOA/ABP/Correctness.ML
--- a/src/HOL/IOA/ABP/Correctness.ML	Tue Apr 23 16:58:21 1996 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML	Tue Apr 23 16:58:57 1996 +0200
@@ -227,6 +227,9 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) sender_ioa sender_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
+by (rtac conjI 1);
+(* start states *)
+by (fast_tac set_cs 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -239,6 +242,9 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) receiver_ioa receiver_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
+by (rtac conjI 1);
+ (* start states *)
+by (fast_tac set_cs 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -250,6 +256,9 @@
 goal Correctness.thy 
       "is_weak_pmap (%id.id) env_ioa env_ioa";
 by (simp_tac (!simpset addsimps [Solve.is_weak_pmap_def]) 1);
+by (rtac conjI 1);
+(* start states *)
+by (fast_tac set_cs 1);
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);