--- a/Nominal/Fv.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Fv.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -92,12 +92,10 @@
 
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
-(* Currently needs just one full_tname to access Datatype *)
-fun define_fv_alpha full_tname bindsall lthy =
+fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy =
 let
   val thy = ProofContext.theory_of lthy;
-  val {descr, ...} = Datatype.the_info thy full_tname;
-  val sorts = []; (* TODO *)
+  val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);

--- a/Nominal/LFex.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/LFex.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -19,11 +19,11 @@
   | Lam "rty" "name" "rtrm"
 
 
-setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *}
 print_theorems
 
 local_setup {*
-  snd o define_fv_alpha "LFex.rkind"
+  snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind")
   [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
    [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
    [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}

--- a/Nominal/Lift.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Lift.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -7,7 +7,7 @@
 
 datatype rtrm2 =
   rVr2 "name"
-| rAp2 "rtrm2" "rtrm2"
+| rAp2 "rtrm2" "rtrm2 list"
 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"
 and ras =
   rAs "name" "rtrm2"
@@ -45,6 +45,10 @@
              [[[], []]]  (*, [[], [[], []]] *) ];
 val bv_simps = @{thms rbv2.simps}
 val info = Datatype.the_info @{theory} ftname;
+*}
+
+.
+{*
 val descr = #descr info;
 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 val full_tnames = List.take (all_full_tnames, length tnames);

--- a/Nominal/Perm.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Perm.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -54,12 +54,11 @@
 *}
 
 ML {*
-(* TODO: full_name can be obtained from new_type_names with Datatype *)
-fun define_raw_perms new_type_names full_tnames thy =
+fun define_raw_perms (dt_info : info) number thy =
 let
-  val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames);
-  (* TODO: [] should be the sorts that we'll take from the specification *)
-  val sorts = [];
+  val {descr, induct, sorts, ...} = dt_info;
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
+  val full_tnames = List.take (all_full_tnames, number);
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "permute_" ^ name_of_typ (nth_dtyp i)) descr);
@@ -101,8 +100,8 @@
     val ((perm_frees, perm_ldef), lthy') =
       Primrec.add_primrec
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
-    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names);
-    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names)
+    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number);
+    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number)
     val perms_name = space_implode "_" perm_names'
     val perms_zero_bind = Binding.name (perms_name ^ "_zero")
     val perms_append_bind = Binding.name (perms_name ^ "_append")

--- 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)]]],
   [[], [[]], [[], []]]] *}
 

--- a/Nominal/Term2.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term2.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -20,9 +20,9 @@
 where
   "rbv2 (rAs x t) = {atom x}"
 
-setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Term2.rtrm2", "Term2.rassign"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *}
 
-local_setup {* snd o define_fv_alpha "Term2.rtrm2"
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2")
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],
    [[[], []]]] *}
 

--- a/Nominal/Term3.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term3.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -22,9 +22,9 @@
   "bv3 rANil = {}"
 | "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"
 
-setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Term3.rtrm3", "Term3.rassigns"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *}
 
-local_setup {* snd o define_fv_alpha "Term3.rtrm3"
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3")
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
    [[], [[], [], []]]] *}
 print_theorems

--- 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

--- a/Nominal/Term5.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term5.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -19,10 +19,10 @@
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
 
-setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Term5.rtrm5", "Term5.rlts"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}
 print_theorems
 
-local_setup {* snd o define_fv_alpha "Term5.rtrm5" [
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [
   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
 print_theorems
 

--- 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

--- a/Nominal/Term7.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term7.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -18,10 +18,10 @@
 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
 
-setup {* snd o define_raw_perms ["rtrm7"] ["Term7.rtrm7"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term7.rtrm7") 1 *}
 thm permute_rtrm7.simps
 
-local_setup {* snd o define_fv_alpha "Term7.rtrm7" [
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term7.rtrm7") [
   [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
 print_theorems
 notation

--- 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

--- a/Nominal/Term9.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Term9.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -16,10 +16,10 @@
   "rbv9 (Var9 x) = {}"
 | "rbv9 (Lam9 x b) = {atom x}"
 
-setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Term9.rlam9", "Term9.rbla9"] *}
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term9.rlam9") 2 *}
 print_theorems
 
-local_setup {* snd o define_fv_alpha "Term9.rlam9" [
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term9.rlam9") [
   [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *}
 notation
   alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and

--- 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
 *)