--- a/Nominal/Term3.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term3.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -22,9 +22,9 @@
   "bv3 rANil = {}"
 | "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"
 
-setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Term3.rtrm3", "Term3.rassigns"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *}
 
-local_setup {* snd o define_fv_alpha "Term3.rtrm3"
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3")
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
    [[], [[], [], []]]] *}
 print_theorems