--- a/Nominal/nominal_dt_rawfuns.ML	Sun Dec 12 00:10:40 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Sun Dec 12 22:09:11 2010 +0000
@@ -13,11 +13,12 @@
   (* info of raw binding functions *)
   type bn_info = term * int * (int * term option) list list
 
-  
   (* binding modes and binding clauses *)
   datatype bmode = Lst | Res | Set
   datatype bclause = BC of bmode * (term option * int) list * int list
 
+  val get_all_binders: bclause list -> (term option * int) list
+
   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) 
@@ -57,6 +58,12 @@
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
+fun get_all_binders bclauses = 
+  bclauses
+  |> map (fn (BC (_, x, _)) => x) 
+  |> flat
+  |> remove_dups (op =)
+
 fun lookup xs x = the (AList.lookup (op=) xs x)