--- a/Nominal/Ex/SingleLet.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -36,11 +36,6 @@
 thm single_let.supp
 thm single_let.fresh
 
-primrec
-  permute_bn_raw
-where
-  "permute_bn_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"
-
 quotient_definition
   "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"
 is