diff -r 98a290c4b0b4 -r 2a1eef99bb6a src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Apr 03 16:20:34 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Tue Apr 03 17:05:52 2007 +0200
@@ -81,10 +81,6 @@
 defs (unchecked overloaded)
   perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
 
-lemma swap_fun: 
-  shows "[(a,b)]\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. [(a,b)]\<bullet>f([(a,b)]\<bullet>x))"
-by (unfold perm_fun_def,auto)
-
 (* permutation on bools *)
 primrec (unchecked perm_bool)
   true_eqvt:  "pi\<bullet>True  = True"