--- a/Nominal/Ex/Foo1.thy	Sat Nov 13 10:25:03 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sat Nov 13 22:23:26 2010 +0000
@@ -42,20 +42,6 @@
 thm foo.supp
 thm foo.fresh
 
-quotient_definition
-  "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg"
-is
-  "permute_bn1_raw"
-
-quotient_definition
-  "permute_bn2 :: perm \<Rightarrow> assg \<Rightarrow> assg"
-is
-  "permute_bn2_raw"
-
-quotient_definition
-  "permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg"
-is
-  "permute_bn3_raw"
 
 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted]
 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted]