--- a/Nominal/Test.thy	Thu Mar 18 18:43:21 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 19:02:33 2010 +0100
@@ -108,10 +108,10 @@
   shows "P c lm"
 proof -
   have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm_induct)
-    apply(simp only: lm_perm)
+    apply(induct lm arbitrary: c rule: lm.induct)
+    apply(simp only: lm.perm)
     apply(rule a1)
-    apply(simp only: lm_perm)
+    apply(simp only: lm.perm)
     apply(rule a2)
     apply(blast)[1]
     apply(assumption)
@@ -121,7 +121,7 @@
     apply(rule_tac t="p \<bullet> Lm name lm" and 
                    s="q \<bullet> p \<bullet> Lm name lm" in subst)
     defer
-    apply(simp add: lm_perm)
+    apply(simp add: lm.perm)
     apply(rule a3)
     apply(simp add: eqvts fresh_star_def)
     apply(drule_tac x="q + p" in meta_spec)
@@ -651,6 +651,28 @@
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
 
+lemma
+"fv_mexp j = supp j \<and> fv_body k = supp k \<and> 
+(fv_defn c = supp c \<and> fv_cbinders c = {a. infinite {b. \<not>alpha_cbinders ((a \<rightleftharpoons> b) \<bullet> c) c}}) \<and>
+fv_sexp d = supp d \<and> fv_sbody e = supp e \<and> 
+(fv_spec l = supp l \<and> fv_Cbinders l = {a. infinite {b. \<not>alpha_Cbinders ((a \<rightleftharpoons> b) \<bullet> l) l}}) \<and>
+fv_tyty g = supp g \<and> fv_path h = supp h \<and> fv_trmtrm i = supp i"
+apply(induct rule: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct)
+apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv)
+apply(simp_all only: supp_Abs[symmetric])
+apply(simp_all (no_asm) only: supp_def)
+apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm)
+apply(simp_all only: permute_ABS)
+apply(simp_all only: mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff Abs_eq_iff)
+apply(simp_all only: alpha_gen)
+apply(simp_all only: eqvts[symmetric] supp_Pair)
+apply(simp_all only: eqvts Pair_eq)
+apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
+apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
+apply(simp_all only: de_Morgan_conj[symmetric])
+apply simp_all
+done
+
 (* example 3 from Peter Sewell's bestiary *)
 
 nominal_datatype exp =