--- a/Nominal/Term5.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term5.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -19,10 +19,10 @@
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
 
-setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Term5.rtrm5", "Term5.rlts"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}
 print_theorems
 
-local_setup {* snd o define_fv_alpha "Term5.rtrm5" [
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [
   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
 print_theorems