--- a/Nominal/nominal_dt_rawfuns.ML	Sun Aug 22 14:02:49 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Wed Aug 25 09:02:06 2010 +0800
@@ -7,9 +7,13 @@
 
 signature NOMINAL_DT_RAWFUNS =
 sig
-  (* info of binding functions *)
+  (* info of raw datatypes *)
+  type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list
+
+  (* info of raw binding functions *)
   type bn_info = (term * int * (int * term option) list list) list
 
+  
   (* binding modes and binding clauses *)
   datatype bmode = Lst | Res | Set
   datatype bclause = BC of bmode * (term option * int) list * int list
@@ -24,6 +28,11 @@
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
+  (* TODO: should be here
+  val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->
+    (Attrib.binding * term) list -> thm list -> thm list -> local_theory ->
+    (term list * thm list * bn_info * thm list * local_theory) *)
+
   val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
     thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
  
@@ -34,6 +43,14 @@
 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
 struct
 
+(* string list      - type variables of a datatype
+   binding          - name of the datatype
+   mixfix           - its mixfix
+   (binding * typ list * mixfix) list  - datatype constructors of the type
+*)  
+type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list
+
+
 (* term              - is constant of the bn-function 
    int               - is datatype number over which the bn-function is defined
    int * term option - is number of the corresponding argument with possibly
@@ -41,6 +58,7 @@
 *)  
 type bn_info = (term * int * (int * term option) list list) list
 
+
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
@@ -127,6 +145,7 @@
   else t
 
 
+
 (** functions that construct the equations for fv and fv_bn **)
 
 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
@@ -239,12 +258,12 @@
   val {fs, simps, inducts, ...} = info;
 
   val morphism = ProofContext.export_morphism lthy'' lthy
-  val fs_exp = map (Morphism.term morphism) fs
   val simps_exp = map (Morphism.thm morphism) (the simps)
   val inducts_exp = map (Morphism.thm morphism) (the inducts)
-  val (fvs_exp, fv_bns_exp) = chop (length fv_frees) fs_exp
+
+  val (fvs', fv_bns') = chop (length fv_frees) fs
 in
-  (fvs_exp, fv_bns_exp, simps_exp, inducts_exp, lthy'')
+  (fvs', fv_bns', simps_exp, inducts_exp, lthy'')
 end