--- a/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 17:52:25 2010 +0800
@@ -24,9 +24,8 @@
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
-  val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
-    bclause list list list -> thm list -> Proof.context -> 
-    term list * term list * thm list * thm list * local_theory
+  val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
+    thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
  
   val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
 end
@@ -211,26 +210,23 @@
   map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 
-fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =
+fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms lthy =
 let
-  val fv_names = prefix_dt_names descr sorts "fv_"
-  val fv_arg_tys = all_dtyps descr sorts
-  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
+  val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
+  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
   val fv_frees = map Free (fv_names ~~ fv_tys);
-  val fv_map = fv_arg_tys ~~ fv_frees
+  val fv_map = raw_tys ~~ fv_frees
 
   val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
   val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
   val fv_bn_names = map (prefix "fv_") bn_names
-  val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
+  val fv_bn_arg_tys = map (nth raw_tys) bn_tys
   val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
   val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
   val fv_bn_map = bns ~~ fv_bn_frees
 
-  val constrs_info = all_dtyp_constrs_types descr sorts
-
-  val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss 
-  val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info
+  val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss 
+  val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info
   
   val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)