# HG changeset patch
# User paulson
# Date 1036169034 -3600
# Node ID a6bc3001106a5e61ebae1fbcba4822cf03fd2288
# Parent  ac335b2f4a39ba4cad2153f55b83ef48cd09ef70
tidy

diff -r ac335b2f4a39 -r a6bc3001106a src/ZF/Constructible/Separation.thy
--- 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