src/HOL/Nominal/Nominal.thy

--- a/src/HOL/Nominal/Nominal.thy	Mon Jun 12 18:17:21 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Jun 12 20:32:33 2006 +0200
@@ -235,6 +235,10 @@
   shows "a\<sharp>{x} = a\<sharp>x"
   by (simp add: fresh_def supp_singleton)
 
+lemma fresh_unit:
+  shows "a\<sharp>()"
+  by (simp add: fresh_def supp_unit)
+
 lemma fresh_prod:
   fixes a :: "'x"
   and   x :: "'a"