--- a/Nominal/Ex/Ex1.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Ex/Ex1.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -6,7 +6,7 @@
 
 atom_decl name
 
-declare [[STEPS = 100]]
+thm finite_sets_supp
 
 nominal_datatype foo =
   Foo0 "name"

--- a/Nominal/Ex/Foo2.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -21,10 +21,12 @@
 binder
   bn::"assg \<Rightarrow> atom list"
 where
- "bn (As x y t a) = [atom x] @ bn a"
+  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
 
+
+
 thm foo.bn_defs
 thm foo.permute_bn
 thm foo.perm_bn_alpha
@@ -69,65 +71,26 @@
 *)
 
 
-text {* *}
 
 
 
-(*
-thm at_set_avoiding1[THEN exE]
-
-
-lemma Let1_rename:
-  fixes c::"'a::fs"
-  shows "\<exists>name' trm'. {atom name'} \<sharp>* c \<and>  Lam name trm = Lam name' trm'"
-apply(simp only: foo.eq_iff)
-apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE])
-apply(simp)
-apply(simp add: finite_supp)
-apply(perm_simp)
-apply(rule Abs_rename_list[THEN exE])
-apply(simp only: set_eqvt)
-apply
-sorry 
-*)
-
-thm foo.exhaust
-
-ML {*
-fun strip_prems_concl trm =
-  (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
-*}
-
-ML {*
-  @{thms foo.exhaust}
-  |> map prop_of
-  |> map strip_prems_concl
-  |> map fst
-  |> map (map (Syntax.string_of_term @{context}))
-  |> map cat_lines
-  |> cat_lines
-  |> writeln 
-*}
-
 lemma test6:
   fixes c::"'a::fs"
-  assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
-  and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
+  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
   and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
-  and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"
+  and     "\<And>a1 trm1 a2 trm2.  \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P"
   and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
   shows "P"
-apply(rule_tac foo.exhaust(1))
+apply(rule_tac y="y" in foo.exhaust(1))
 apply(rule assms(1))
-apply(rule exI)+
 apply(assumption)
 apply(rule assms(2))
-apply(rule exI)+
 apply(assumption)
 (* lam case *)
 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
 apply(erule exE)
-apply(insert Abs_rename_list)[1]
+apply(insert Abs_rename_lst)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name]" in meta_spec)
 apply(drule_tac x="trm" in meta_spec)
@@ -150,12 +113,18 @@
 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")
 apply(erule exE)
 apply(rule assms(4))
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair)
+apply(erule conjE)+
+apply(assumption)
+apply(simp only:)
 apply(simp only: foo.eq_iff)
-apply(insert Abs_rename_list)[1]
+(* *)
+apply(insert Abs_rename_lst)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg1" in meta_spec)
 apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_list)[1]
+apply(insert Abs_rename_lst)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg2" in meta_spec)
 apply(drule_tac x="trm2" in meta_spec)
@@ -164,21 +133,18 @@
 apply(drule meta_mp)
 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
 apply(erule exE)+
-apply(rule exI)+
 apply(perm_simp add: foo.permute_bn)
-apply(rule conjI)
-apply(simp add: fresh_star_Pair fresh_star_Un)
+apply(simp add: fresh_star_Pair)
 apply(erule conjE)+
+apply(rule assms(4))
+apply(assumption)
+apply(simp add: foo.eq_iff refl)
 apply(rule conjI)
-apply(assumption)
-apply(rotate_tac 4)
-apply(assumption)
-apply(rule conjI)
-apply(assumption)
+apply(rule refl)
 apply(rule conjI)
 apply(rule foo.perm_bn_alpha)
 apply(rule conjI)
-apply(assumption)
+apply(rule refl)
 apply(rule foo.perm_bn_alpha)
 apply(rule at_set_avoiding1)
 apply(simp)

--- a/Nominal/Ex/TypeSchemes.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -9,6 +9,8 @@
 
 (* defined as a single nominal datatype *)
 
+thm finite_set
+
 nominal_datatype ty =
   Var "name"
 | Fun "ty" "ty"

--- a/Nominal/Nominal2.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Nominal2.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -6,6 +6,7 @@
      ("nominal_dt_quot.ML")
 begin
 
+
 use "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
 
@@ -50,9 +51,10 @@
 
 
 ML {*
-fun process_ecase lthy c (params, prems, concl) binders =
+fun process_ecase lthy c (params, prems, concl) bclauses =
   let
     val tys = map snd params
+    val binders = get_all_binders bclauses
    
     fun prep_binder (opt, i) = 
       let
@@ -77,15 +79,21 @@
   end  
 *}
 
+
 ML {*
-fun fresh_thm ctxt c params binders bn_finite_thms =
+fun fresh_thm ctxt c parms binders bn_finite_thms =
   let
     fun prep_binder (opt, i) = 
       case opt of
-        NONE => setify ctxt (nth params i) 
-      | SOME bn => to_set (bn $ (nth params i))    
+        NONE => setify ctxt (nth parms i) 
+      | SOME bn => to_set (bn $ (nth parms i))  
 
-    val rhs = HOLogic.mk_tuple (c :: params)
+    fun prep_binder2 (opt, i) = 
+      case opt of
+        NONE => atomify ctxt (nth parms i)
+      | SOME bn => bn $ (nth parms i) 
+
+    val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders))
     val lhs = binders
       |> map prep_binder
       |> fold_union
@@ -94,33 +102,99 @@
     val goal = mk_fresh_star lhs rhs
       |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t))
       |> HOLogic.mk_Trueprop   
-    val ss = @{thms finite.emptyI finite.insertI finite_supp supp_Pair finite_Un finite_fset finite_set} 
-      @ bn_finite_thms  
+ 
+    val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} 
+      @ @{thms finite.intros finite_Un finite_set finite_fset}  
   in
     Goal.prove ctxt [] [] goal
       (K (HEADGOAL (rtac @{thm at_set_avoiding1}
           THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss)))))
   end
+
+fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) =
+  case binders of
+    [] => [] 
+  | binders =>
+      let
+        val binder_trm = Nominal_Dt_Alpha.comb_binders ctxt bmode parms binders
+        val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
+        val body_ty = fastype_of body_trm
+
+        val (abs_name, binder_ty, abs_ty) = 
+          case bmode of
+            Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
+          | Set => (@{const_name "Abs_set"}, @{typ "atom set"},  @{type_name abs_set})
+          | Res => (@{const_name "Abs_res"}, @{typ "atom set"},  @{type_name abs_res})
+
+        val abs = Const (abs_name, [binder_ty, body_ty] ---> Type (abs_ty, [body_ty]))
+        val abs_lhs = abs $ binder_trm $ body_trm
+        val abs_rhs = abs $ mk_perm p binder_trm $ Bound 0
+        val goal = HOLogic.mk_eq (abs_lhs, abs_rhs)
+          |> (fn t => HOLogic.mk_exists ("y", body_ty, t))
+          |> HOLogic.mk_Trueprop  
+ 
+        val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
+          @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
+          fresh_star_set} @ @{thms finite.intros finite_fset}  
+     in
+       [Goal.prove ctxt [] [] goal
+          (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst}
+              THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] 
+     end
+*}
+
+ML {* 
+fun partitions [] [] = []
+  | partitions xs (i :: js) = 
+      let
+        val (head, tail) = chop i xs
+      in
+        head :: partitions tail js
+      end
+*}
+
+
+ML {*
+fun mk_cperm ctxt p ctrm =
+  mk_perm (term_of p) (term_of ctrm)
+  |> cterm_of (ProofContext.theory_of ctxt)
+*}
+
+
+ML {*
+fun case_tac ctxt c bn_finite_thms (prems, bclausess) thm =
+  let
+    fun aux_tac prem bclauses =
+      case (get_all_binders bclauses) of
+        [] => EVERY' [rtac prem, atac]
+      | binders => Subgoal.FOCUS (fn {params, prems, context = ctxt, ...} =>  
+          let
+            val parms = map (term_of o snd) params
+            val fthm = fresh_thm ctxt c parms binders bn_finite_thms 
+  
+            val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
+            val (([(_, fperm)], fprops), ctxt') = Obtain.result
+              (K (EVERY1 [etac exE, 
+                          full_simp_tac (HOL_basic_ss addsimps ss), 
+                          REPEAT o (etac conjE)])) [fthm] ctxt 
+            (*
+            val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops))
+            *)    
+            val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses)
+            (* 
+            val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs))
+            *)
+          in
+            (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*)
+            Skip_Proof.cheat_tac (ProofContext.theory_of ctxt')
+          end) ctxt
+  in
+    rtac thm THEN' RANGE (map2 aux_tac prems bclausess)
+  end
 *}
 
 
 ML {*
-fun case_tac ctxt c bn_finite_thms binderss thm =
-  let
-    fun aux_tac (binders : (term option * int) list)=
-      Subgoal.FOCUS (fn {params, context, ...} =>  
-        let
-          val prms = map (term_of o snd) params
-          val fthm = fresh_thm ctxt c prms binders bn_finite_thms
-          val _ = tracing ("params" ^ @{make_string} params) 
-          val _ = tracing ("binders" ^ @{make_string} binders) 
-        in
-          Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
-        end) ctxt
-  in
-    rtac thm THEN' RANGE (map aux_tac binderss)
-  end
-
 fun prove_strong_exhausts lthy qexhausts qtrms bclausesss bn_finite_thms =
   let
     val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy 
@@ -128,22 +202,22 @@
     val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
     val c = Free (c, TFree (a, @{sort fs}))
 
-    val binderss = map (map get_all_binders) bclausesss
-
     val (ecases, main_concls) = qexhausts' (* ecases or of the form (params, prems, concl) *)
       |> map prop_of
       |> map Logic.strip_horn
       |> split_list
       |>> map (map strip_params_prems_concl)     
 
-    val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat binderss)
-
-    val _ = tracing ("binderss: " ^ @{make_string} binderss)     
+    val prems = map2 (process_ecase lthy'' c) (flat ecases) (flat bclausesss)
   in
     Goal.prove_multi lthy'' [] prems main_concls
-     (fn {prems, context} => 
-        EVERY1 [Goal.conjunction_tac,
-                RANGE (map2 (case_tac context c bn_finite_thms) binderss qexhausts')])
+     (fn {prems:thm list, context} =>
+        let
+           val prems' = partitions prems (map length bclausesss)
+        in
+          EVERY1 [Goal.conjunction_tac,
+            RANGE (map2 (case_tac context c bn_finite_thms) (prems' ~~ bclausesss) qexhausts')]
+        end)
   end
 *}
 
@@ -323,7 +397,7 @@
   val raw_induct_thm = #induct dtinfo
   val raw_induct_thms = #inducts dtinfo
   val raw_exhaust_thms = map #exhaust dtinfos
-  val raw_size_trms = map size_const raw_tys
+  val raw_size_trms = map HOLogic.size_const raw_tys
   val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
     |> `(fn thms => (length thms) div 2)
     |> uncurry drop

--- a/Nominal/Nominal2_Abs.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -587,7 +587,7 @@
   then show "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y" by blast
 qed
 
-lemma Abs_rename_list:
+lemma Abs_rename_lst:
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" 
   shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y"

--- a/Nominal/Nominal2_Base.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -1411,6 +1411,16 @@
 unfolding fresh_star_def
 by (simp add: fresh_set)
 
+lemma fresh_star_singleton:
+  fixes a::"atom"
+  shows "as \<sharp>* {a} \<longleftrightarrow> as \<sharp>* a"
+  by (simp add: fresh_star_def fresh_finite_insert fresh_set_empty)
+
+lemma fresh_star_fset:
+  fixes xs::"('a::fs) list"
+  shows "as \<sharp>* fset S \<longleftrightarrow> as \<sharp>* S"
+by (simp add: fresh_star_def fresh_def) 
+
 lemma fresh_star_Un:
   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
   by (auto simp add: fresh_star_def)
@@ -1701,7 +1711,6 @@
 
 section {* Renaming permutations *}
 
-
 lemma set_renaming_perm:
   assumes a: "p \<bullet> bs \<inter> bs = {}" 
   and     b: "finite bs"
@@ -1840,6 +1849,10 @@
   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"
   by (simp add: fresh_def supp_at_base supp_atom)
 
+lemma fresh_star_atom_at_base: 
+  fixes b::"'a::at_base"
+  shows "as \<sharp>* atom b \<longleftrightarrow> as \<sharp>* b"
+  by (simp add: fresh_star_def fresh_atom_at_base)
 
 instance at_base < fs
 proof qed (simp add: supp_at_base)

--- a/Nominal/nominal_dt_alpha.ML	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Thu Dec 16 08:42:48 2010 +0000
@@ -7,6 +7,8 @@
 
 signature NOMINAL_DT_ALPHA =
 sig
+  val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term
+
   val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> 
     bclause list list list -> term list -> Proof.context -> 
     term list * term list * thm list * thm list * thm * local_theory
@@ -71,7 +73,7 @@
   end
 
 (* generates the compound binder terms *)
-fun mk_binders lthy bmode args binders = 
+fun comb_binders lthy bmode args binders = 
   let  
     fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
       | bind_set _ args (SOME bn, i) = bn $ (nth args i)
@@ -150,8 +152,8 @@
           val comp_alpha = foldl1 mk_prod_alpha alphas
           val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)
           val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)
-          val comp_binders = mk_binders lthy bmode args binders
-          val comp_binders' = mk_binders lthy bmode args' binders
+          val comp_binders = comb_binders lthy bmode args binders
+          val comp_binders' = comb_binders lthy bmode args' binders
           val alpha_prem = 
             mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'
           val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)

--- a/Nominal/nominal_dt_rawfuns.ML	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Dec 16 08:42:48 2010 +0000
@@ -60,7 +60,7 @@
 
 fun get_all_binders bclauses = 
   bclauses
-  |> map (fn (BC (_, x, _)) => x) 
+  |> map (fn (BC (_, binders, _)) => binders) 
   |> flat
   |> remove_dups (op =)
 

--- 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