src/HOL/Nominal/Nominal.thy

--- a/src/HOL/Nominal/Nominal.thy	Mon Jun 12 22:14:38 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Jun 13 15:07:47 2006 +0200
@@ -698,7 +698,7 @@
   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