--- a/Nominal-General/nominal_library.ML	Thu May 20 21:23:53 2010 +0100
+++ b/Nominal-General/nominal_library.ML	Thu May 20 21:35:00 2010 +0100
@@ -28,6 +28,10 @@
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 
+  val mk_diff: term * term -> term
+  val mk_union: term * term -> term
+  val fold_union: term list -> term
+
   (* datatype operations *)
   val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
   val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
@@ -74,6 +78,21 @@
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 
+(* functions that construct differences and unions
+   but avoid producing empty atom sets *)
+
+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_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)  
+ 
+fun fold_union trms = fold (curry mk_union) trms @{term "{}::atom set"}
+
+
 (** datatypes **)