--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 18:17:53 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Wed Aug 18 00:19:15 2010 +0800
@@ -6,6 +6,7 @@
 
 declare [[STEPS = 20]]
 
+
 nominal_datatype trm  =
   Var "name"
 | App "trm" "trm"
@@ -21,6 +22,8 @@
 where
   "bn (As x y t) = {atom x}"
 
+
+
 ML {* Function.prove_termination *}
 
 text {* can lift *}
@@ -29,14 +32,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