--- a/Quot/Nominal/Nominal2_Supp.thy	Sun Feb 07 10:16:21 2010 +0100
+++ b/Quot/Nominal/Nominal2_Supp.thy	Sun Feb 07 10:20:29 2010 +0100
@@ -153,7 +153,7 @@
       thus "h a = h b" by simp
     next
       assume "a \<noteq> b"
-      hence "atom a \<sharp> b" by (simp add: fresh_at)
+      hence "atom a \<sharp> b" by (simp add: fresh_at_base)
       with a3 have "atom a \<sharp> h b" by (rule fresh_apply)
       with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
         by (rule swap_fresh_fresh)