src/ZF/Constructible/WF_absolute.thy

--- a/src/ZF/Constructible/WF_absolute.thy	Wed Jul 24 16:16:44 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jul 24 17:59:12 2002 +0200
@@ -568,7 +568,7 @@
 apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
        in rspec [THEN rspec]) 
 apply (simp_all add: function_lam) 
-apply (blast intro: dest: pair_components_in_M ) 
+apply (blast intro: lam_closed dest: pair_components_in_M ) 
 done
 
 text{*Eliminates one instance of replacement.*}