--- a/Nominal/nominal_library.ML	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/nominal_library.ML	Thu Dec 16 08:42:48 2010 +0000
@@ -18,8 +18,6 @@
   val mk_id: term -> term
   val mk_all: (string * typ) -> term -> term
 
-  val size_const: typ -> term 
-
   val sum_case_const: typ -> typ -> typ -> term
   val mk_sum_case: term -> term -> term
  
@@ -49,10 +47,11 @@
   val is_atom_fset: Proof.context -> typ -> bool
   val is_atom_list: Proof.context -> typ -> bool
 
-  val to_atom_set: term -> term
   val to_set_ty: typ -> term -> term
   val to_set: term -> term
   
+  val atomify_ty: Proof.context -> typ -> term -> term
+  val atomify: Proof.context -> term -> term
   val setify_ty: Proof.context -> typ -> term -> term
   val setify: Proof.context -> term -> term
   val listify_ty: Proof.context -> typ -> term -> term
@@ -125,19 +124,18 @@
 fun order eq keys list = 
   map (the o AList.lookup eq list) keys
 
+(* remove duplicates *)
 fun remove_dups eq [] = []
-  | remove_dups eq (x::xs) = 
-      if (member eq xs x) 
+  | remove_dups eq (x :: xs) = 
+      if member eq xs x 
       then remove_dups eq xs 
-      else x::(remove_dups eq xs)
-
+      else x :: remove_dups eq xs
 
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)
   | last2 (_ :: xs) = last2 xs
 
-
 fun is_true @{term "Trueprop True"} = true
   | is_true _ = false 
 
@@ -148,6 +146,7 @@
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
 
+
 fun mk_id trm =
   let 
     val ty = fastype_of trm
@@ -157,11 +156,9 @@
 
 fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)
 
-
-fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})
-
 fun sum_case_const ty1 ty2 ty3 = 
   Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
+
 fun mk_sum_case trm1 trm2 =
   let
     val ([ty1], ty3) = strip_type (fastype_of trm1)
@@ -192,19 +189,18 @@
 
 fun mk_atom_set_ty ty t =
   let
-    val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
-    val img_ty = atom_ty --> ty --> @{typ "atom set"};
+    val atom_ty = HOLogic.dest_setT ty 
+    val img_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom set"};
   in
-    Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
+    Const (@{const_name image}, img_ty) $ atom_const atom_ty $ t
   end
 
 fun mk_atom_fset_ty ty t =
   let
     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)
+    Const (@{const_name map_fset}, fmap_ty) $ atom_const atom_ty $ t
   end
 
 fun mk_atom_list_ty ty t =
@@ -212,7 +208,7 @@
     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
+    Const (@{const_name map}, map_ty) $ atom_const atom_ty $ t
   end
 
 fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t
@@ -220,11 +216,12 @@
 fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t
 
 (* coerces a list into a set *)
-fun to_atom_set t = @{term "set :: atom list => atom set"} $ t
   
 fun to_set_ty ty t =
-  if ty = @{typ "atom list"}
-  then to_atom_set t else t
+  case ty of
+    @{typ "atom list"} => @{term "set :: atom list => atom set"} $ t
+  | @{typ "atom fset"} => @{term "fset :: atom fset => atom set"} $ t
+  | _ => t
 
 fun to_set t = to_set_ty (fastype_of t) t
 
@@ -243,22 +240,30 @@
   | is_atom_list _ _ = false
 
 
-(* functions that coerces singletons, sets and fsets of concrete atoms
-   into sets of general atoms *)
+(* functions that coerce singletons, sets, fsets and lists of concrete 
+   atoms into general atoms sets / lists *)
+fun atomify_ty ctxt ty t =
+  if is_atom ctxt ty
+    then  mk_atom_ty ty t
+  else if is_atom_set ctxt ty
+    then mk_atom_set_ty ty t
+  else if is_atom_fset ctxt ty
+    then mk_atom_fset_ty ty t
+  else if is_atom_list ctxt ty
+    then mk_atom_list_ty ty t
+  else raise TERM ("atomify", [t])
+
 fun setify_ty ctxt ty t =
   if is_atom ctxt ty
     then  HOLogic.mk_set @{typ atom} [mk_atom_ty ty t]
   else if is_atom_set ctxt ty
     then mk_atom_set_ty ty t
   else if is_atom_fset ctxt ty
-    then mk_atom_fset_ty ty t
+    then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t
   else if is_atom_list ctxt ty
-    then to_atom_set (mk_atom_list_ty ty t)
+    then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t
   else raise TERM ("setify", [t])
 
-
-(* functions that coerces singletons and lists of concrete atoms
-   into lists of general atoms  *)
 fun listify_ty ctxt ty t =
   if is_atom ctxt ty
     then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t]
@@ -266,7 +271,8 @@
     then mk_atom_list_ty ty t
   else raise TERM ("listify", [t])
 
-fun setify ctxt t = setify_ty ctxt (fastype_of t) t
+fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t
+fun setify ctxt t  = setify_ty ctxt (fastype_of t) t
 fun listify ctxt t = listify_ty ctxt (fastype_of t) t
 
 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool}
@@ -422,7 +428,7 @@
            SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT)
       | (Type (@{type_name Product_Type.prod}, [fT, sT])) =>
            prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT)
-      | _ => size_const T
+      | _ => HOLogic.size_const T
 
     fun mk_measure_trm T = 
       HOLogic.dest_setT T