src/HOL/Nominal/Nominal.thy

   hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove)
   have "(UNIV-{a}) \<noteq> ({}::'x set)" 
   proof (rule_tac ccontr, drule_tac notnotD)
     assume "UNIV-{a} = ({}::'x set)"
     with inf2 have "infinite ({}::'x set)" by simp
-    then show "False" by (auto intro: infinite_nonempty)
+    then show "False" by auto
   qed
   hence "\<exists>(b::'x). b\<in>(UNIV-{a})" by blast
   then obtain b::"'x" where mem2: "b\<in>(UNIV-{a})" by blast
   from mem2 have "a\<noteq>b" by blast
   then show "\<exists>(b::'x). a\<noteq>b" by blast