--- a/Nominal/Ex/Let.thy	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Ex/Let.thy	Mon Sep 27 12:19:17 2010 -0400
@@ -27,26 +27,8 @@
 thm trm_assn.inducts
 thm trm_assn.distinct
 thm trm_assn.supp
-
-
-lemma supp_fresh_eq:
-  assumes "supp x = supp y"
-  shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y"
-using assms by (simp add: fresh_def)
+thm trm_assn.fresh
 
-lemma supp_not_in:
-  assumes "x = y"
-  shows "a \<notin> x \<longleftrightarrow> a \<notin> y"
-using assms
-by (simp add: fresh_def)
-
-lemmas freshs =
-  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))"
@@ -83,7 +65,7 @@
 apply(simp)
 apply(rule test_trm_test_assn.intros)
 apply(assumption)
-apply(simp add: freshs fresh_star_def)
+apply(simp add: trm_assn.fresh fresh_star_def)
 apply(simp)
 defer
 apply(simp)
@@ -93,10 +75,11 @@
 apply(assumption)
 apply(assumption)
 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
-apply(rule eq_iffs(4)[THEN iffD2])
+apply(rule trm_assn.eq_iff(4)[THEN iffD2])
 defer
 apply(rule test_trm_test_assn.intros)
 prefer 3
+apply(simp add: fresh_star_def trm_assn.fresh)
 thm freshs
 --"HERE"