--- a/Nominal/Ex/Lambda.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -3,7 +3,7 @@
 begin
 
 atom_decl name
-declare [[STEPS = 20]]
+declare [[STEPS = 21]]
 
 class s1
 class s2
@@ -14,88 +14,16 @@
 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
 | Lam x::"name" l::"('a, 'b) lam"  bind x in l
 
-term Var_raw
-term Var
-term App_raw
-term App
-thm Var_def App_def Lam_def
-term abs_lam
-
 thm distinct
-thm lam_raw.inducts
-thm lam_raw.exhaust
+thm induct
+thm exhaust
 thm fv_defs
 thm bn_defs
 thm perm_simps
-thm perm_laws
-thm lam_raw.size
 thm eq_iff
-thm eq_iff_simps
-thm fv_eqvt
-thm bn_eqvt
+thm fv_bn_eqvt
 thm size_eqvt
 
-ML {*
-  val qtys = [@{typ "('a::{s1, fs}, 'b::{s2,fs}) lam"}]
-*}
-
-ML {*
-  val thm_a = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.induct}
-*}
-
-ML {* 
-  val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.exhaust}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}
-*}
-
-ML {*
-  val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{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} qtys simps)  @{thms eq_iff}
-*}
-
-ML {*
- val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff_simps}
-*}
-
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}
-*}
-
-ML {*
-  val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}
-*}
-
-
-
-thm eq_iff
 
 thm lam.fv
 thm lam.supp