
diff -r cbcd4997dac5 -r 22a084c9316b Nominal/LFex.thy
--- a/Nominal/LFex.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 02 11:04:49 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)




