diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Mon May 24 20:02:37 2010 +0100
@@ -13,6 +13,8 @@
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind_set x in t
 | Let a::"assg" t::"trm"  bind_set "bn a" in t
+| Foo x::"name" y::"name" t::"trm" bind_set x in y t
+| Bar x::"name" y::"name" t::"trm" bind y x in t x y
 and assg =
   As "name" "trm"
 binder
@@ -20,10 +22,12 @@
 where
   "bn (As x t) = {atom x}"
 
+
 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
 
 
+
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv
 thm trm_assg.supp