--- a/Nominal/NewFv.thy	Tue Apr 27 23:11:40 2010 +0200
+++ b/Nominal/NewFv.thy	Wed Apr 28 06:24:10 2010 +0200
@@ -12,17 +12,16 @@
 *}
 
 ML {*
-  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
+fun mk_singleton_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
 
-  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
+val noatoms = @{term "{} :: atom set"};
 
-  val noatoms = @{term "{} :: atom set"};
-  fun mk_union sets =
-    fold (fn a => fn b =>
-      if a = noatoms then b else
-      if b = noatoms then a else
-      if a = b then a else
-      HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
+fun mk_union sets =
+  fold (fn a => fn b =>
+  if a = noatoms then b else
+  if b = noatoms then a else
+  if a = b then a else
+  HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
 *}
 
 ML {*
@@ -66,7 +65,7 @@
   val ty = fastype_of t;
 in
   if is_atom thy ty 
-    then mk_single_atom t 
+    then mk_singleton_atom t 
   else if is_atom_set thy ty 
     then mk_atom_set t 
   else if is_atom_fset thy ty 
@@ -90,7 +89,9 @@
       val x = nth args i;
       val dt = nth dts i;
     in
-      if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
+      if Datatype_Aux.is_rec_type dt 
+      then nth fv_frees (Datatype_Aux.body_index dt) $ x 
+      else atoms thy x
     end
   val fv_bodys = mk_union (map fv_body bodys)
   val bound_vars =
@@ -118,7 +119,9 @@
       val dt = nth dts i;
     in
       case AList.lookup (op=) args_in_bn i of
-        NONE => if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
+        NONE => if Datatype_Aux.is_rec_type dt 
+                then nth fv_frees (Datatype_Aux.body_index dt) $ x 
+                else atoms thy x
       | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
       | SOME NONE => noatoms
     end
@@ -132,13 +135,12 @@
   bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
 let
   val {descr, sorts, ...} = dt_info;
-  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
   let
-    val Ts = map (typ_of_dtyp descr sorts) dts;
+    val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
     val names = Datatype_Prop.make_tnames Ts;
     val args = map Free (names ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+    val c = Const (cname, Ts ---> (nth_dtyp descr sorts ith_dtyp));
     val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn
   in
     HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -176,7 +178,9 @@
       val x = nth args i;
       val dt = nth dts i;
     in
-      if is_rec_type dt then nth fv_frees (body_index dt) $ x else atoms thy x
+      if Datatype_Aux.is_rec_type dt 
+      then nth fv_frees (Datatype_Aux.body_index dt) $ x 
+      else atoms thy x
     end
 | BLst (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y
@@ -187,13 +191,12 @@
 fun fv thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
 let
   val {descr, sorts, ...} = dt_info;
-  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   fun fv_constr (cname, dts) bml =
   let
-    val Ts = map (typ_of_dtyp descr sorts) dts;
+    val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
     val names = Datatype_Prop.make_tnames Ts;
     val args = map Free (names ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+    val c = Const (cname, Ts ---> (nth_dtyp descr sorts ith_dtyp));
     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
   in
     HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -216,24 +219,26 @@
   #> Proof.global_terminal_proof (Method.Basic method, NONE)
 *}
 
-
-
 ML {*
 fun define_raw_fv dt_info bns bmlll lthy =
 let
   val thy = ProofContext.theory_of lthy;
   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);
-  val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
+    "fv_" ^ Datatype_Aux.name_of_typ (nth_dtyp descr sorts i)) descr);
+
+  val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
   val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll;
+
   val fvbns = map snd bn_fvbn;
   val fv_nums = 0 upto (length fv_frees - 1)
+
   val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bmlll (fv_frees ~~ fv_nums);
   val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)
+
   val lthy' =
     lthy
     |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config