diff -r e965524c3301 -r 003c7e290a04 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 02 15:07:27 2010 +0100
@@ -24,9 +24,9 @@
 
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind")
-  [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
-   [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
-   [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+  [[ [], [(NONE, 1, 2)]],
+   [ [], [], [(NONE, 1, 2)] ],
+   [ [], [], [], [(NONE, 1, 2)]]] *}
 notation
     alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)
 and alpha_rty    ("_ \<approx>ty _" [100, 100] 100)