Proof modification.

--- a/src/HOL/IOA/ABP/Correctness.ML	Mon Mar 04 14:37:33 1996 +0100
+++ b/src/HOL/IOA/ABP/Correctness.ML	Mon Mar 04 14:38:30 1996 +0100
@@ -270,6 +270,7 @@
 by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
 qed"env_unchanged";
 
+Delsimps [Collect_False_empty];
 
 goal Correctness.thy "compat_ioas srch_ioa rsch_ioa"; 
 by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1);