src/HOL/Nominal/Nominal.thy
changeset 41550 efa734d9b221
parent 41413 64cd30d6b0b8
child 41562 90fb3d7474df
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -785,7 +785,7 @@
     1.4    hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
     1.5    then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force
     1.6    then have "c\<notin>A" by simp
     1.7 -  then show ?thesis using prems by simp 
     1.8 +  then show ?thesis ..
     1.9  qed
    1.10  
    1.11  text {* there always exists a fresh name for an object with finite support *}