--- a/Nominal/Term6.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Term6.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -22,7 +22,7 @@
 print_theorems
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
+  [[], [(NONE, 0, 1)], [(SOME @{term rbv6}, 0, 1)]]] *}
 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
 thm alpha_rtrm6.intros
 
@@ -41,7 +41,7 @@
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []),
   build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt))
 *}
-
+thm alpha6_eqvt
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []),
   (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *}
 thm alpha6_equivp