diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term2.thy
--- a/Nominal/Term2.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term2.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -20,9 +20,9 @@
 where
   "rbv2 (rAs x t) = {atom x}"
 
-setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Term2.rtrm2", "Term2.rassign"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *}
 
-local_setup {* snd o define_fv_alpha "Term2.rtrm2"
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2")
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
    [[[], []]]] *}