diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/TySch.thy
--- a/Nominal/TySch.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/TySch.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -9,21 +9,22 @@
   Var "name"
 | Fun "ty" "ty"
 
-setup {* snd o define_raw_perms ["ty"] ["TySch.ty"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.ty") 1 *}
 print_theorems
 
 datatype tyS =
   All "name set" "ty"
 
-setup {* snd o define_raw_perms ["tyS"] ["TySch.tyS"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "TySch.tyS") 1 *}
 print_theorems
 
-local_setup {* snd o define_fv_alpha "TySch.ty" [[[[]], [[], []]]] *}
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "TySch.ty")
+ [[[[]], [[], []]]] *}
 print_theorems
 
 (*
 Doesnot work yet since we do not refer to fv_ty
-local_setup {* define_raw_fv "TySch.tyS" [[[[], []]]] *}
+local_setup {* define_raw_fv (Datatype.the_info @{theory} "TySch.tyS") [[[[], []]]] *}
 print_theorems
 *)