diff -r be087f48b99f -r 2cf506c09946 src/ZF/Constructible/WFrec.thy
--- a/src/ZF/Constructible/WFrec.thy	Mon Nov 18 14:51:44 2002 +0100
+++ b/src/ZF/Constructible/WFrec.thy	Tue Nov 19 10:41:20 2002 +0100
@@ -105,7 +105,7 @@
 apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
 apply (rename_tac x1)
 apply (rule_tac t="%z. H(x1,z)" in subst_context) 
-apply (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g")
+apply (subgoal_tac "\<forall>y \<in> r-``{x1}. ALL z. <y,z>\<in>f <-> <y,z>\<in>g")
  apply (blast intro: transD) 
 apply (simp add: apply_iff) 
 apply (blast intro: transD sym)