diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Term4.thy
--- a/Nominal/Term4.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term4.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -16,7 +16,7 @@
 
 (* there cannot be a clause for lists, as *)
 (* permutations are  already defined in Nominal (also functions, options, and so on) *)
-setup {* snd o define_raw_perms ["rtrm4"] ["Term4.rtrm4"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
 
 (* "repairing" of the permute function *)
 lemma repaired:
@@ -29,8 +29,8 @@
 thm permute_rtrm4_permute_rtrm4_list.simps
 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
-local_setup {* snd o define_fv_alpha "Term4.rtrm4" [
-  [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
 print_theorems
 
 notation