--- a/Nominal/Ex/SingleLet.thy	Sun Aug 22 14:02:49 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Wed Aug 25 09:02:06 2010 +0800
@@ -6,8 +6,7 @@
 
 declare [[STEPS = 20]]
 
-
-nominal_datatype trm  =
+nominal_datatype singlelet: trm  =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind x in t
@@ -23,8 +22,6 @@
   "bn (As x y t) = {atom x}"
 
 
-ML {* Function.prove_termination *}
-
 text {* can lift *}
 
 thm distinct
@@ -32,6 +29,7 @@
 thm trm_raw.exhaust
 thm assg_raw.exhaust
 thm fv_defs
+thm bn_defs
 thm perm_simps
 thm perm_laws
 thm trm_raw_assg_raw.size(9 - 16)
@@ -42,8 +40,6 @@
 thm bn_eqvt
 thm size_eqvt
 
-ML {* lift_thm *}
-
 
 ML {*
   val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct})
@@ -108,6 +104,7 @@
 
 
 
+
 lemma supp_fv:
   "supp t = fv_trm t"
   "supp b = fv_bn b"