--- a/Nominal/Rsp.thy	Sat Mar 27 12:26:59 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 27 13:50:59 2010 +0100
@@ -94,8 +94,6 @@
 in
   Const (@{const_name permute}, @{typ perm} --> ty --> ty)
 end
-
-val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
 *}
 
 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"