tidy

--- a/src/ZF/Constructible/Separation.thy	Fri Nov 01 13:16:28 2002 +0100
+++ b/src/ZF/Constructible/Separation.thy	Fri Nov 01 17:43:54 2002 +0100
@@ -64,8 +64,7 @@
 apply (drule subset_Lset_ltD, assumption)
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule collI)
-apply assumption
+apply (rule collI, assumption)
 done
 
 text{*As above, but typically @{term u} is a finite enumeration such as