diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term6.thy
--- a/Nominal/Term6.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term6.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -18,10 +18,10 @@
 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
 
-setup {* snd o define_raw_perms ["rtrm6"] ["Term6.rtrm6"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term6.rtrm6") 1 *}
 print_theorems
 
-local_setup {* snd o define_fv_alpha "Term6.rtrm6" [
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [
   [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *}
 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100)
 thm alpha_rtrm6.intros