--- a/Nominal/Ex/Let.thy	Mon Sep 27 04:56:49 2010 -0400
+++ b/Nominal/Ex/Let.thy	Mon Sep 27 09:51:15 2010 -0400
@@ -18,36 +18,21 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
+
 thm trm_assn.fv_defs
-thm trm_assn.eq_iff trm_assn.bn_defs
+thm trm_assn.eq_iff 
 thm trm_assn.bn_defs
 thm trm_assn.perm_simps
-thm trm_assn.induct[no_vars]
-thm trm_assn.inducts[no_vars]
+thm trm_assn.induct
+thm trm_assn.inducts
 thm trm_assn.distinct
 thm trm_assn.supp
-thm trm_assn.fv_defs[simplified trm_assn.supp(1-2)]
 
 
-
-lemma fv_supp:
-  shows "fv_trm = supp"
-  and   "fv_assn = supp"
-apply(rule ext)
-apply(rule trm_assn.supp)
-apply(rule ext)
-apply(rule trm_assn.supp)
-done
-
-lemmas eq_iffs = trm_assn.eq_iff[folded fv_supp[symmetric], folded Abs_eq_iff]
-
-lemmas supps = trm_assn.fv_defs[simplified trm_assn.supp(1-2)]
-
 lemma supp_fresh_eq:
   assumes "supp x = supp y"
   shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y"
-using assms
-by (simp add: fresh_def)
+using assms by (simp add: fresh_def)
 
 lemma supp_not_in:
   assumes "x = y"
@@ -56,12 +41,12 @@
 by (simp add: fresh_def)
 
 lemmas freshs =
-  supps(1)[THEN supp_not_in, folded fresh_def]
-  supps(2)[THEN supp_not_in, simplified, folded fresh_def]
-  supps(3)[THEN supp_not_in, folded fresh_def]
-  supps(4)[THEN supp_not_in, folded fresh_def]
-  supps(5)[THEN supp_not_in, simplified, folded fresh_def]
-  supps(6)[THEN supp_not_in, simplified, folded fresh_def]
+  trm_assn.supp(1)[THEN supp_not_in, folded fresh_def]
+  trm_assn.supp(2)[THEN supp_not_in, simplified, folded fresh_def]
+  trm_assn.supp(3)[THEN supp_not_in, folded fresh_def]
+  trm_assn.supp(4)[THEN supp_not_in, folded fresh_def]
+  trm_assn.supp(5)[THEN supp_not_in, simplified, folded fresh_def]
+  trm_assn.supp(6)[THEN supp_not_in, simplified, folded fresh_def]
 
 lemma fin_bn:
   shows "finite (set (bn l))"