--- a/Nominal/Term9.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term9.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -16,10 +16,10 @@
   "rbv9 (Var9 x) = {}"
 | "rbv9 (Lam9 x b) = {atom x}"
 
-setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Term9.rlam9", "Term9.rbla9"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term9.rlam9") 2 *}
 print_theorems
 
-local_setup {* snd o define_fv_alpha "Term9.rlam9" [
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term9.rlam9") [
   [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
 notation
   alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and