--- a/Nominal/Ex/Foo1.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -42,21 +42,6 @@
 thm foo.supp
 thm foo.fresh
 
-primrec
-  permute_bn1_raw
-where
-  "permute_bn1_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"
-
-primrec
-  permute_bn2_raw
-where
-  "permute_bn2_raw p (As_raw x y t) = As_raw x (p \<bullet> y) t"
-
-primrec
-  permute_bn3_raw
-where
-  "permute_bn3_raw p (As_raw x y t) = As_raw (p \<bullet> x) (p \<bullet> y) t"
-
 quotient_definition
   "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg"
 is