# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274387700 -3600
# Node ID bf748be701094f8c67680086ba98803781c16651
# Parent  3b83960f95446a1389b3bbb34514d4eeebdf1642
moved some mk_union and mk_diff into the library

diff -r 3b83960f9544 -r bf748be70109 Nominal-General/nominal_library.ML
--- 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 **)
 
 
diff -r 3b83960f9544 -r bf748be70109 Nominal/nominal_dt_rawfuns.ML
--- 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})