src/HOL/ZF/HOLZF.thy

 lemma PFun_inj: "Elem F (PFun U V) \<Longrightarrow> Elem x F \<Longrightarrow> Elem y F \<Longrightarrow> Fst x = Fst y \<Longrightarrow> Snd x = Snd y"
   apply (frule Elem_Elem_PFun[where p=x], simp)
   apply (frule Elem_Elem_PFun[where p=y], simp)
   apply (subgoal_tac "isFun F")
   apply (simp add: isFun_def isOpair_def)  
-  apply (auto simp add: Fst Snd, blast)
+  apply (auto simp add: Fst Snd)
   apply (auto simp add: PFun_def Sep)
   done
 
 lemma Fun_total: "\<lbrakk>Elem F (Fun U V); Elem a U\<rbrakk> \<Longrightarrow> \<exists>x. Elem (Opair a x) F"
   using [[simp_depth_limit = 2]]