diff -r 8aff3f3ce47f -r 45a69c9cc4cc Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal-General/nominal_library.ML	Mon May 24 20:02:37 2010 +0100
@@ -22,6 +22,7 @@
   val mk_atom: term -> term
 
   val supp_ty: typ -> typ
+  val supp_const: typ -> term
   val mk_supp_ty: typ -> term -> term
   val mk_supp: term -> term
 
@@ -29,15 +30,17 @@
   val safe_mk_equiv: thm -> thm
 
   val mk_diff: term * term -> term
+  val mk_append: term * term -> term
   val mk_union: term * term -> term
   val fold_union: term list -> term
 
   (* datatype operations *)
+  val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
   val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
   val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
-    (term * typ * typ list) list list
+    (term * typ * typ list * bool list) list list
   val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> 
-    (term * typ * typ list) list
+    (term * typ * typ list * bool list) list
   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
 
 end
@@ -61,7 +64,6 @@
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t]);
 
-
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
 fun atom_ty ty = ty --> @{typ "atom"};
@@ -70,7 +72,8 @@
 
 
 fun supp_ty ty = ty --> @{typ "atom set"};
-fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t;
+fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty)
+fun mk_supp_ty ty t = supp_const ty $ t;
 fun mk_supp t = mk_supp_ty (fastype_of t) t;
 
 
@@ -78,25 +81,35 @@
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 
-(* functions that construct differences and unions
-   but avoid producing empty atom sets *)
+(* functions that construct differences, appends and unions
+   but avoid producing empty atom sets or empty atom lists *)
 
 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
   | mk_diff (t1, @{term "{}::atom set"}) = t1
   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
 
+fun mk_append (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"}
+  | mk_append (t1, @{term "[]::atom list"}) = t1
+  | mk_append (@{term "[]::atom list"}, t2) = t2
+  | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) 
+
 fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
   | mk_union (t1 , @{term "{}::atom set"}) = t1
   | mk_union (@{term "{}::atom set"}, t2) = t2
-  | mk_union (t1, t2) = HOLogic.mk_binop @{const_name sup} (t1, t2)  
+  | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  
  
 fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
 
 
+
+
 (** datatypes **)
 
 
 (* returns the type of the nth datatype *)
+fun all_dtyps descr sorts = 
+  map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1))
+
 fun nth_dtyp descr sorts n = 
   Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
 
@@ -113,8 +126,9 @@
     val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs
     val ty = Type (ty_name, vs_tys)
     val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args
+    val is_rec = map Datatype_Aux.is_rec_type args
   in
-    (Const (cname, arg_tys ---> ty), ty, arg_tys)
+    (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec)
   end
 in
   map (map aux) (all_dtyp_constrs_info descr)