diff -r ebf253d80670 -r 0f24c961b5f6 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Fri Jul 30 00:40:32 2010 +0100
+++ b/Nominal-General/nominal_library.ML	Sat Jul 31 01:24:39 2010 +0100
@@ -35,6 +35,8 @@
   val mk_append: term * term -> term
   val mk_union: term * term -> term
   val fold_union: term list -> term
+  val mk_conj: term * term -> term
+  val fold_conj: term list -> term
 
   (* datatype operations *)
   val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
@@ -102,20 +104,21 @@
   | 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
+fun 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
+fun 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_rev (curry mk_union) trms @{term "{}::atom set"}
 
+fun mk_conj (t1, @{term "True"}) = t1
+  | mk_conj (@{term "True"}, t2) = t2
+  | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2)
 
-
+fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
 
 (** datatypes **)