diff -r d5713db7e146 -r dd7490fdd998 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Sun Dec 19 07:50:37 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Dec 21 10:28:08 2010 +0000
@@ -18,6 +18,7 @@
   datatype bclause = BC of bmode * (term option * int) list * int list
 
   val get_all_binders: bclause list -> (term option * int) list
+  val is_recursive_binder: bclause -> bool
 
   val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> thm list -> thm list -> local_theory ->
@@ -64,6 +65,12 @@
   |> flat
   |> remove_dups (op =)
 
+fun is_recursive_binder (BC (_, binders, bodies)) =
+  case (inter (op =) (map snd binders) bodies) of
+    nil => false
+  | _ => true
+  
+
 fun lookup xs x = the (AList.lookup (op=) xs x)