--- a/Nominal/nominal_dt_rawfuns.ML	Thu May 20 21:23:53 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu May 20 21:35:00 2010 +0100
@@ -16,7 +16,6 @@
 
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
-  val fold_union: term list -> term
 
   val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list ->
     (term * 'a * 'b) list -> (term * int * (int * term option) list list) list ->
@@ -30,21 +29,6 @@
 datatype bmode = Lst | Res | Set
 datatype bclause = BC of bmode * (term option * int) list * int list
 
-(* 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"}
-
-
 (* atom types *)
 fun is_atom ctxt ty =
   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})