--- a/Nominal/nominal_dt_rawfuns.ML	Wed Dec 08 12:37:25 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Wed Dec 08 13:05:04 2010 +0000
@@ -8,7 +8,7 @@
 signature NOMINAL_DT_RAWFUNS =
 sig
   (* info of raw datatypes *)
-  type dt_info = string list * binding * mixfix * ((binding * typ list * mixfix) list) list
+  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
@@ -28,11 +28,10 @@
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
-  (* FIXME: should be here - currently in Nominal2.thy
   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 list * thm list * local_theory) 
-  *)
+
 
   val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> 
     thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
@@ -55,7 +54,7 @@
    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
+type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
 
 
 (* term              - is constant of the bn-function 
@@ -149,6 +148,88 @@
   end
 
 
+(** functions that define the raw binding functions **)
+
+(* strip_bn_fun takes a rhs of a bn function: this can only contain unions or
+   appends of elements; in case of recursive calls it returns also the applied
+   bn function *)
+fun strip_bn_fun lthy args t =
+let 
+  fun aux t =
+    case t of
+      Const (@{const_name sup}, _) $ l $ r => aux l @ aux r
+    | Const (@{const_name append}, _) $ l $ r => aux l @ aux r
+    | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+        (find_index (equal x) args, NONE) :: aux y
+    | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+        (find_index (equal x) args, NONE) :: aux y
+    | Const (@{const_name bot}, _) => []
+    | Const (@{const_name Nil}, _) => []
+    | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)]
+    | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t))
+in
+  aux t
+end  
+
+(** definition of the raw binding functions **)
+
+fun prep_bn_info lthy dt_names dts bn_funs eqs = 
+let
+  fun process_eq eq = 
+  let
+    val (lhs, rhs) = eq
+      |> HOLogic.dest_Trueprop
+      |> HOLogic.dest_eq
+    val (bn_fun, [cnstr]) = strip_comb lhs
+    val (_, ty) = dest_Const bn_fun
+    val (ty_name, _) = dest_Type (domain_type ty)
+    val dt_index = find_index (fn x => x = ty_name) dt_names
+    val (cnstr_head, cnstr_args) = strip_comb cnstr    
+    val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head))
+    val rhs_elements = strip_bn_fun lthy cnstr_args rhs
+  in
+    ((bn_fun, dt_index), (cnstr_name, rhs_elements))
+  end
+
+  (* order according to constructor names *)
+  fun cntrs_order ((bn, dt_index), data) = 
+  let
+    val dt = nth dts dt_index                      
+    val cts = (fn (_, _, _, x) => x) dt     
+    val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts  
+  in
+    (bn, (bn, dt_index, order (op=) ct_names data))
+  end 
+in
+  eqs
+  |> map process_eq 
+  |> AList.group (op=)      (* eqs grouped according to bn_functions *)
+  |> map cntrs_order        (* inner data ordered according to constructors *)
+  |> order (op=) bn_funs    (* ordered according to bn_functions *)
+end
+
+fun define_raw_bns dt_names dts raw_bn_funs raw_bn_eqs constr_thms size_thms lthy =
+  if null raw_bn_funs 
+  then ([], [], [], [], lthy)
+  else 
+    let
+      val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
+        Function_Common.default_config (pat_completeness_simp constr_thms) lthy
+
+      val (info, lthy2) = prove_termination size_thms (Local_Theory.restore lthy1)
+      val {fs, simps, inducts, ...} = info
+
+      val raw_bn_induct = (the inducts)
+      val raw_bn_eqs = the simps
+
+      val raw_bn_info = 
+        prep_bn_info lthy dt_names dts fs (map prop_of raw_bn_eqs)
+    in
+      (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
+    end
+
+
+
 (** functions that construct the equations for fv and fv_bn **)
 
 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) =