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 ("_ \ki _" [100, 100] 100) and alpha_rty ("_ \ty _" [100, 100] 100)