--- a/Nominal/Term8.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term8.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -17,10 +17,10 @@
   "rbv8 (Bar0 x) = {}"
 | "rbv8 (Bar1 v x b) = {atom v}"
 
-setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Term8.rfoo8", "Term8.rbar8"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *}
 print_theorems
 
-local_setup {* snd o define_fv_alpha "Term8.rfoo8" [
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [
   [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
 notation
   alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and