# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265534429 -3600
# Node ID 2f1377bb4e1f721f5f2db83d5892380a477446f6
# Parent  c70e7545b73851fb727c0c54b49d1163227bbff7
fixed lemma name

diff -r c70e7545b738 -r 2f1377bb4e1f Quot/Nominal/Nominal2_Supp.thy
--- 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)