diff -r f2d4dae2a10b -r 621ebd8b13c4 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sat Aug 21 16:20:10 2010 +0800
@@ -10,9 +10,9 @@
 nominal_datatype trm  =
   Var "name"
 | 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" t1::"trm" t2::"trm" bind_set x in y t t1 t2
+| Lam x::"name" t::"trm"  bind x in t
+| Let a::"assg" t::"trm"  bind (set) "bn a" in t
+| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
 | Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 
 and assg =
@@ -24,6 +24,7 @@
 
 
 
+
 ML {* Function.prove_termination *}
 
 text {* can lift *}
@@ -32,14 +33,14 @@
 thm trm_raw_assg_raw.inducts
 thm trm_raw.exhaust
 thm assg_raw.exhaust
-thm FV_defs
+thm fv_defs
 thm perm_simps
 thm perm_laws
 thm trm_raw_assg_raw.size(9 - 16)
 thm eq_iff
 thm eq_iff_simps
 thm bn_defs
-thm FV_eqvt
+thm fv_eqvt
 thm bn_eqvt
 thm size_eqvt
 
@@ -106,7 +107,6 @@
 
 
 
-
 lemma supp_fv:
   "supp t = fv_trm t"
   "supp b = fv_bn b"