diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/LFex.thy
--- a/Nominal/LFex.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/LFex.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -19,11 +19,11 @@
   | Lam "rty" "name" "rtrm"
 
 
-setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *}
 print_theorems
 
 local_setup {*
-  snd o define_fv_alpha "LFex.rkind"
+  snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind")
   [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
    [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
    [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}