--- a/Nominal/Term7.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term7.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -18,10 +18,10 @@
 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
 
-setup {* snd o define_raw_perms ["rtrm7"] ["Term7.rtrm7"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term7.rtrm7") 1 *}
 thm permute_rtrm7.simps
 
-local_setup {* snd o define_fv_alpha "Term7.rtrm7" [
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term7.rtrm7") [
   [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
 print_theorems
 notation