src/ZF/Constructible/L_axioms.thy

--- a/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Mon Jul 01 18:16:18 2002 +0200
@@ -62,8 +62,7 @@
 
 lemma replacement: "replacement(L,P)"
 apply (simp add: replacement_def, clarify)
-apply (frule LReplace_in_L, assumption+)
-apply clarify 
+apply (frule LReplace_in_L, assumption+, clarify) 
 apply (rule_tac x=Y in exI)   
 apply (simp add: Replace_iff univalent_def, blast) 
 done