--- a/Nominal/Ex/LetRec2.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/Ex/LetRec2.thy	Fri Aug 27 02:03:52 2010 +0800
@@ -4,6 +4,7 @@
 
 atom_decl name
 
+
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -19,14 +20,12 @@
 | "bn (Lcons x t l) = (atom x) # (bn l)"
 
 
-thm trm_lts.fv
+thm trm_lts.fv_defs
 thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
+thm trm_lts.bn_defs
+thm trm_lts.perm_simps
 thm trm_lts.induct
 thm trm_lts.distinct
-thm trm_lts.supp
-thm trm_lts.fv[simplified trm_lts.supp]
 
 
 (* why is this not in HOL simpset? *)
@@ -75,7 +74,7 @@
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
   apply (simp add: atom_eqvt fresh_star_def)
   done
-
+*)
 end