diff -r aa5059a00f41 -r 6fd3fc3254ee Nominal/Ex/LetRec2.thy
--- a/Nominal/Ex/LetRec2.thy	Wed Sep 21 17:16:11 2011 +0900
+++ b/Nominal/Ex/LetRec2.thy	Wed Sep 21 10:23:06 2011 +0200
@@ -5,26 +5,29 @@
 atom_decl name
 
 nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm"  binds (set) x in t
-| Lt a::"lts" t::"trm"   binds "bn a" in a t
-and lts =
-  Lnil
-| Lcons "name" "trm" "lts"
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  binds x in t
+| Let as::"assn" t::"trm"   binds "bn as" in t
+| Let_rec as::"assn" t::"trm"   binds "bn as" in as t
+and assn =
+  ANil
+| ACons "name" "trm" "assn"
 binder
   bn
 where
-  "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
+  "bn (ANil) = []"
+| "bn (ACons x t as) = (atom x) # (bn as)"
 
+thm trm_assn.eq_iff
+thm trm_assn.supp
 
-thm trm_lts.fv_defs
-thm trm_lts.eq_iff
-thm trm_lts.bn_defs
-thm trm_lts.perm_simps
-thm trm_lts.induct
-thm trm_lts.distinct
+thm trm_assn.fv_defs
+thm trm_assn.eq_iff
+thm trm_assn.bn_defs
+thm trm_assn.perm_simps
+thm trm_assn.induct
+thm trm_assn.distinct