diff -r 700024ec18da -r 98303b78fb64 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Wed Apr 28 06:55:07 2010 +0200
+++ b/Nominal/NewFv.thy	Wed Apr 28 07:09:11 2010 +0200
@@ -131,29 +131,28 @@
 *}
 
 ML {*
-fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees
+fun fv_bn thy dt_descr sorts fv_frees
   bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) =
 let
-  val {descr, sorts, ...} = dt_info;
   fun fv_bn_constr (cname, dts) (args_in_bn, bml) =
   let
-    val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
+    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
     val names = Datatype_Prop.make_tnames Ts;
     val args = map Free (names ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp descr sorts ith_dtyp));
+    val c = Const (cname, Ts ---> (nth_dtyp dt_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
       (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
   end;
-  val (_, (_, _, constrs)) = nth descr ith_dtyp;
+  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 in
   map2 fv_bn_constr constrs (args_in_bns ~~ bmll)
 end
 *}
 
 ML {*
-fun fv_bns thy dt_info fv_frees bn_funs bclauses =
+fun fv_bns thy dt_descr sorts fv_frees bn_funs bclauses =
 let
   fun mk_fvbn_free (bn, ith, _) =
     let
@@ -164,7 +163,7 @@
   val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs);
   val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees
   val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs;
-  val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs);
+  val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs);
 in
   (bn_fvbn, fvbn_names, eqs)
 end
@@ -188,21 +187,20 @@
 *}
 
 ML {*
-fun fv thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
+fun fv thy dt_descr sorts fv_frees bn_fvbn bmll (fv_free, ith_dtyp) =
 let
-  val {descr, sorts, ...} = dt_info;
   fun fv_constr (cname, dts) bml =
   let
-    val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
+    val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts;
     val names = Datatype_Prop.make_tnames Ts;
     val args = map Free (names ~~ Ts);
-    val c = Const (cname, Ts ---> (nth_dtyp descr sorts ith_dtyp));
+    val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp));
     val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn
   in
     HOLogic.mk_Trueprop (HOLogic.mk_eq
       (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml)))
   end;
-  val (_, (_, _, constrs)) = nth descr ith_dtyp;
+  val (_, (_, _, constrs)) = nth dt_descr ith_dtyp;
 in
   map2 fv_constr constrs bmll
 end
@@ -220,7 +218,7 @@
 *}
 
 ML {*
-fun define_raw_fv dt_info bn_funs bclauses lthy =
+fun define_raw_fv (dt_info : Datatype_Aux.info)  bn_funs bclauses lthy =
 let
   val thy = ProofContext.theory_of lthy;
   val {descr as dt_descr, sorts, ...} = dt_info;
@@ -230,12 +228,12 @@
   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 bn_funs bclauses;
+    fv_bns thy dt_descr sorts fv_frees bn_funs bclauses;
 
   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) bclauses (fv_frees ~~ fv_nums);
+  val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (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)