--- a/Nominal/Ex/SingleLet.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 20]]
+declare [[STEPS = 21]]
 
 nominal_datatype singlelet: trm  =
   Var "name"
@@ -22,86 +22,17 @@
   "bn (As x y t) = {atom x}"
 
 
-text {* can lift *}
-
 thm distinct
-thm trm_raw_assg_raw.inducts
-thm trm_raw.exhaust
-thm assg_raw.exhaust
+thm induct
+thm exhaust
 thm fv_defs
 thm bn_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 bn_eqvt
+thm fv_bn_eqvt
 thm size_eqvt
 
 
-ML {*
-  val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct})
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw_assg_raw.inducts}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw.exhaust}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms assg_raw.exhaust}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_defs}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms trm_raw_assg_raw.size(9 - 16)}
-*}
-
-ML {*
-  val thms_p = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_simps}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms perm_laws}
-*}
-
-ML {*
-  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
-    prod.cases}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps)  @{thms eq_iff}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} [@{typ trm}, @{typ assg}] simps) @{thms eq_iff_simps}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_defs}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms bn_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms fv_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms size_eqvt}
-*}
-