diff -r 217149972715 -r f4eba60cbd69 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Fri Sep 03 20:53:09 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Fri Sep 03 22:22:43 2010 +0800
@@ -49,6 +49,7 @@
   val mk_append: term * term -> term
   val mk_union: term * term -> term
   val fold_union: term list -> term
+  val fold_append: term list -> term
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
 
@@ -144,6 +145,8 @@
 
 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
   | mk_diff (t1, @{term "{}::atom set"}) = t1
+  | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"}
+  | mk_diff (t1, @{term "set ([]::atom list)"}) = t1
   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
 
 fun mk_append (t1, @{term "[]::atom list"}) = t1
@@ -152,9 +155,12 @@
 
 fun mk_union (t1, @{term "{}::atom set"}) = t1
   | mk_union (@{term "{}::atom set"}, t2) = t2
+  | mk_union (t1, @{term "set ([]::atom list)"}) = t1
+  | mk_union (@{term "set ([]::atom list)"}, 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 fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"}
 
 fun mk_conj (t1, @{term "True"}) = t1
   | mk_conj (@{term "True"}, t2) = t2