src/ZF/Constructible/Wellorderings.thy

--- a/src/ZF/Constructible/Wellorderings.thy	Wed Jan 15 16:44:21 2003 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy	Wed Jan 15 16:45:32 2003 +0100
@@ -84,7 +84,7 @@
 lemma  (in M_basic) wellfounded_on_iff_wellfounded:
      "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
 apply (simp add: wellfounded_on_def wellfounded_def, safe)
- apply blast 
+ apply force
 apply (drule_tac x=x in rspec, assumption, blast) 
 done