# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289783402 0
# Node ID 94750b31a97d468965e2f3a69eb5709013fc12db
# Parent  8193bbaa07feb0f1bda4a7ff3036136b1d7fd0cd
fixed bug in fv function where a shallow binder binds lists of names

diff -r 8193bbaa07fe -r 94750b31a97d Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Sun Nov 14 16:34:47 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon Nov 15 01:10:02 2010 +0000
@@ -101,20 +101,20 @@
 fun mk_atom_fset t =
   let
     val ty = fastype_of t;
-    val atom_ty = dest_fsetT ty --> @{typ "atom"};
-    val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+    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) $ Const (@{const_name atom}, atom_ty) $ t)
+    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 --> @{typ atom};
-    val map_ty = atom_ty --> ty --> @{typ "atom list"};
+    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) $ mk_atom_ty atom_ty t
+    Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t
   end
 
 (* functions that coerces singletons, sets and fsets of concrete atoms
@@ -141,14 +141,14 @@
     if is_atom ctxt ty
       then HOLogic.mk_list @{typ atom} [mk_atom t]
     else if is_atom_list ctxt ty
-      then mk_atom_set t
+      then mk_atom_list t
     else raise TERM ("listify", [t])
   end
 
 (* coerces a list into a set *)
 fun to_set t =
   if fastype_of t = @{typ "atom list"}
-  then @{term "set::atom list => atom set"} $ t
+  then @{term "set :: atom list => atom set"} $ t
   else t
 
 
@@ -272,7 +272,7 @@
 
     val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
       Function_Common.default_config (pat_completeness_simp constr_thms) lthy
-  
+
     val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
  
     val {fs, simps, inducts, ...} = info;
diff -r 8193bbaa07fe -r 94750b31a97d Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Sun Nov 14 16:34:47 2010 +0000
+++ b/Nominal/nominal_library.ML	Mon Nov 15 01:10:02 2010 +0000
@@ -27,6 +27,7 @@
 
   val mk_sort_of: term -> term
   val atom_ty: typ -> typ
+  val atom_const: typ -> term
   val mk_atom_ty: typ -> term -> term
   val mk_atom: term -> term
 
@@ -128,10 +129,10 @@
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
 fun atom_ty ty = ty --> @{typ "atom"};
-fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;
+fun atom_const ty = Const (@{const_name "atom"}, atom_ty ty)
+fun mk_atom_ty ty t = atom_const ty $ t;
 fun mk_atom t = mk_atom_ty (fastype_of t) t;
 
-
 fun supp_ty ty = ty --> @{typ "atom set"};
 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
 fun mk_supp_ty ty t = supp_const ty $ t