--- a/Nominal/nominal_dt_rawfuns.ML	Fri Dec 10 19:01:44 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Sun Dec 12 00:10:40 2010 +0000
@@ -18,21 +18,10 @@
   datatype bmode = Lst | Res | Set
   datatype bclause = BC of bmode * (term option * int) list * int list
 
-  val is_atom: Proof.context -> typ -> bool
-  val is_atom_set: Proof.context -> typ -> bool
-  val is_atom_fset: Proof.context -> typ -> bool
-  val is_atom_list: Proof.context -> typ -> bool
-  val mk_atom_set: term -> term
-  val mk_atom_fset: term -> term
-
-  val setify: Proof.context -> term -> term
-  val listify: Proof.context -> term -> term
-
   val define_raw_bns: string list -> dt_info -> (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> thm list -> thm list -> local_theory ->
     (term list * thm list * bn_info list * thm list * local_theory) 
 
-
   val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info list -> bclause list list list -> 
     thm list -> thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
 
@@ -71,83 +60,6 @@
 fun lookup xs x = the (AList.lookup (op=) xs x)
 
 
-(* testing for concrete atom types *)
-fun is_atom ctxt ty =
-  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
-
-fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
-  | is_atom_set _ _ = false;
-
-fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
-  | is_atom_fset _ _ = false;
-
-fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
-  | is_atom_list _ _ = false
-
-
-(* functions for producing sets, fsets and lists of general atom type
-   out from concrete atom types *)
-fun mk_atom_set t =
-  let
-    val ty = fastype_of t;
-    val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
-    val img_ty = atom_ty --> ty --> @{typ "atom set"};
-  in
-    Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
-  end
-
-
-fun dest_fsetT (Type (@{type_name fset}, [T])) = T
-  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
-
-fun mk_atom_fset t =
-  let
-    val ty = fastype_of t;
-    val atom_ty = dest_fsetT ty
-    val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"};
-    val fset = @{term "fset :: atom fset => atom set"}
-  in
-    fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t)
-  end
-
-  fun mk_atom_list t =
-  let
-    val ty = fastype_of t
-    val atom_ty = dest_listT ty
-    val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"}
-  in
-    Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t
-  end
-
-(* functions that coerces singletons, sets and fsets of concrete atoms
-   into sets of general atoms *)
-fun setify ctxt t =
-  let
-    val ty = fastype_of t;
-  in
-    if is_atom ctxt ty
-      then  HOLogic.mk_set @{typ atom} [mk_atom t]
-    else if is_atom_set ctxt ty
-      then mk_atom_set t
-    else if is_atom_fset ctxt ty
-      then mk_atom_fset t
-    else raise TERM ("setify", [t])
-  end
-
-(* functions that coerces singletons and lists of concrete atoms
-   into lists of general atoms  *)
-fun listify ctxt t =
-  let
-    val ty = fastype_of t;
-  in
-    if is_atom ctxt ty
-      then HOLogic.mk_list @{typ atom} [mk_atom t]
-    else if is_atom_list ctxt ty
-      then mk_atom_list t
-    else raise TERM ("listify", [t])
-  end
-
-
 (** functions that define the raw binding functions **)
 
 (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or