--- a/Nominal/Term1.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term1.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -27,11 +27,11 @@
 | "bv1 (BVr x) = {atom x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
-setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Term1.rtrm1", "Term1.bp"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *}
 thm permute_rtrm1_permute_bp.simps
 
 local_setup {*
-  snd o define_fv_alpha "Term1.rtrm1"
+  snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
   [[], [[]], [[], []]]] *}