--- a/Nominal/Ex/Let.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal/Ex/Let.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -18,6 +18,8 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
+thm permute_bn_raw.simps
+
 thm at_set_avoiding2
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff 
@@ -30,12 +32,6 @@
 thm trm_assn.fresh
 thm trm_assn.exhaust[where y="t", no_vars]
 
-primrec
-  permute_bn_raw
-where
-  "permute_bn_raw p (ANil_raw) = ANil_raw"
-| "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)"
-
 quotient_definition
   "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
 is