diff -r 8557af71724e -r 0203cd5cfd6c Nominal/Term2.thy
--- a/Nominal/Term2.thy	Mon Mar 01 14:26:14 2010 +0100
+++ b/Nominal/Term2.thy	Mon Mar 01 16:04:03 2010 +0100
@@ -23,8 +23,11 @@
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *}
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2")
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
-   [[[], []]]] *}
+  [[[],
+    [],
+    [(NONE, 0, 1)],
+    [(SOME @{term rbv2}, 0, 1)]],
+   [[]]] *}
 
 notation
   alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and