--- a/Nominal/Manual/Term4.thy	Tue May 04 16:59:31 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Tue May 04 17:15:21 2010 +0200
@@ -1,5 +1,5 @@
 theory Term4
-imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove"
+imports "../NewAlpha" "../Abs" "../Perm" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove"
 begin
 
 atom_decl name
@@ -31,10 +31,13 @@
 thm permute_rtrm4_permute_rtrm4_list.simps
 lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
+ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *}
 
-local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
-  [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *}
-print_theorems
+local_setup {* fn ctxt => let val (_, _, ctxt') = define_raw_fv descr sorts [] bl ctxt in ctxt' end *}
+thm fv_rtrm4.simps fv_rtrm4_list.simps
+
+local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *}
+thm alpha_rtrm4_alpha_rtrm4_list.intros
 
 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"
 apply (rule ext)+
@@ -49,8 +52,6 @@
 apply simp_all
 done
 
-ML {* @{term "\<Union>a"} *}
-
 lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
 apply (rule ext)
 apply (induct_tac x)
@@ -67,7 +68,7 @@
 
 lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3]
 
-local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
+local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
 thm eqvts(1-2)
 
 local_setup {*
@@ -154,7 +155,7 @@
 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
 
 ML {*
-  map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4_fv_rtrm4_list.simps[simplified fix3]}
+  map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fix3] fv_rtrm4_list.simps[simplified fix3]}
 *}
 
 ML {*