diff -r c785fff02a8f -r 8a98171ba1fc Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Thu May 27 18:40:10 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Mon May 31 19:57:29 2010 +0200
@@ -4,6 +4,8 @@
 
 atom_decl name
 
+ML {*  Function.add_function *}
+
 ML {* print_depth 50 *}
 declare [[STEPS = 8]]
 
@@ -22,7 +24,6 @@
 where
   "bn (As x t) = {atom x}"
 
-
 thm permute_trm_raw_permute_assg_raw.simps[no_vars]
 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
@@ -30,32 +31,13 @@
 ML {* val {inducts, ... } = Function.get_info @{context} @{term "fv_trm_raw"}*}
 ML {* Rule_Cases.strict_mutual_rule @{context} (the inducts) *}
 
-(*
-lemma empty_eqvt[eqvt]:
-  shows "p \<bullet> {} = {}"
-  unfolding empty_def
-  by (perm_simp) (rule refl)
-*)
-lemma 
-  "(p \<bullet> {}) = {}"
-thm eqvts_raw
-thm eqvts
-apply(perm_strict_simp)
-
-
 lemma
  shows "p1 \<bullet> fv_trm_raw trm_raw = fv_trm_raw (p1 \<bullet> trm_raw)"
  and "p1 \<bullet> fv_assg_raw assg_raw = fv_assg_raw (p1 \<bullet> assg_raw)"
  and "p1 \<bullet> fv_bn_raw assg_raw = fv_bn_raw (p1 \<bullet> assg_raw)"
 apply(induct trm_raw and assg_raw and assg_raw rule: fv_trm_raw_fv_assg_raw_fv_bn_raw.induct)
-apply(simp_all)
-apply(perm_simp)
-apply(rule refl)
-apply(perm_simp)
-apply(rule refl)
-apply(perm_simp)
-apply(rule refl)
-apply(simp add: fv_trm_raw.simps)
+apply(perm_simp add: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps, rule refl)+
+done