--- a/Nominal-General/Nominal2_Atoms.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -17,7 +17,6 @@
 *}
 
 lemma atom_image_cong:
-  fixes X Y::"('a::at_base) set"
   shows "(atom ` X = atom ` Y) = (X = Y)"
   apply(rule inj_image_eq_iff)
   apply(simp add: inj_on_def)
@@ -33,91 +32,22 @@
   done
 
 lemma supp_finite_at_set:
-  fixes S::"('a::at) set"
-  assumes a: "finite S"
-  shows "supp S = atom ` S"
-  apply(rule finite_supp_unique)
-  apply(simp add: supports_def)
-  apply(rule allI)+
-  apply(rule impI)
-  apply(rule swap_fresh_fresh)
-  apply(simp add: fresh_def)
-  apply(simp add: atom_image_supp)
-  apply(subst supp_finite_atom_set)
-  apply(rule finite_imageI)
-  apply(simp add: a)
-  apply(simp)
-  apply(simp add: fresh_def)
-  apply(simp add: atom_image_supp)
-  apply(subst supp_finite_atom_set)
-  apply(rule finite_imageI)
-  apply(simp add: a)
-  apply(simp)
-  apply(rule finite_imageI)
-  apply(simp add: a)
-  apply(drule swap_set_in)
-  apply(assumption)
-  apply(simp)
-  apply(simp add: image_eqvt)
-  apply(simp add: permute_fun_def)
-  apply(simp add: atom_eqvt)
-  apply(simp add: atom_image_cong)
-  done
-
-lemma supp_finite_at_set_aux:
-  fixes S::"('a::at) set"
   assumes a: "finite S"
   shows "supp S = atom ` S"
-proof
-  show "supp S \<subseteq> ((atom::'a::at \<Rightarrow> atom) ` S)" 
-    apply(rule supp_is_subset)
-    apply(simp add: supports_def)
-    apply(rule allI)+
-    apply(rule impI)
-    apply(rule swap_fresh_fresh)
-    apply(simp add: fresh_def)
-    apply(simp add: atom_image_supp)
-    apply(subst supp_finite_atom_set)
-    apply(rule finite_imageI)
-    apply(simp add: a)
-    apply(simp)
-    apply(simp add: fresh_def)
-    apply(simp add: atom_image_supp)
-    apply(subst supp_finite_atom_set)
-    apply(rule finite_imageI)
-    apply(simp add: a)
-    apply(simp)
-    apply(rule finite_imageI)
-    apply(simp add: a)
-    done
-next 
-  have "supp ((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp ((op `) (atom::'a::at \<Rightarrow> atom)) \<union> supp S"
-    by (simp add: supp_fun_app)
-  moreover
-  have "supp ((op `) (atom::'a::at \<Rightarrow> atom)) = {}"
-    apply(rule supp_fun_eqvt)
-    apply(perm_simp)
-    apply(simp)
-    done
-  moreover 
-  have "supp ((atom::'a::at \<Rightarrow> atom) ` S) = ((atom::'a::at \<Rightarrow> atom) ` S)" 
-    apply(subst supp_finite_atom_set)
-    apply(rule finite_imageI)
-    apply(simp add: a)
-    apply(simp)
-    done
-  ultimately 
-  show "((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp S" by simp
+proof -
+  have fin: "finite (atom ` S)" 
+    using a by (simp add: finite_imageI) 
+  have "supp S = supp (atom ` S)" by (rule atom_image_supp)
+  also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
+  finally show "supp S = atom ` S" by simp
 qed
-  
 
 lemma supp_at_insert:
-  fixes S::"('a::at) set"
+  fixes a::"'a::at_base"
   assumes a: "finite S"
   shows "supp (insert a S) = supp a \<union> supp S"
   using a by (simp add: supp_finite_at_set supp_at_base)
 
-
 section {* A swapping operation for concrete atoms *}
   
 definition

--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -1162,6 +1162,44 @@
   thus ?thesis ..
 qed
 
+lemma image_eqvt:
+  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+  unfolding permute_set_eq_image
+  unfolding permute_fun_def [where f=f]
+  by (simp add: image_image)
+
+lemma atom_image_cong:
+  shows "(atom ` X = atom ` Y) = (X = Y)"
+  apply(rule inj_image_eq_iff)
+  apply(simp add: inj_on_def)
+  done
+
+lemma atom_image_supp:
+  shows "supp S = supp (atom ` S)"
+  apply(simp add: supp_def)
+  apply(simp add: image_eqvt)
+  apply(subst (2) permute_fun_def)
+  apply(simp add: atom_eqvt)
+  apply(simp add: atom_image_cong)
+  done
+
+lemma supp_finite_at_set:
+  assumes a: "finite S"
+  shows "supp S = atom ` S"
+proof -
+  have fin: "finite (atom ` S)" 
+    using a by (simp add: finite_imageI) 
+  have "supp S = supp (atom ` S)" by (rule atom_image_supp)
+  also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
+  finally show "supp S = atom ` S" by simp
+qed
+
+lemma supp_at_insert:
+  fixes a::"'a::at_base"
+  assumes a: "finite S"
+  shows "supp (insert a S) = supp a \<union> supp S"
+  using a by (simp add: supp_finite_at_set supp_at_base)
+
 section {* library functions for the nominal infrastructure *}
 use "nominal_library.ML"
 

--- a/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -152,12 +152,6 @@
   unfolding vimage_def permute_fun_def [where f=f]
   unfolding Collect_eqvt2 mem_eqvt ..
 
-lemma image_eqvt:
-  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
-  unfolding permute_set_eq_image
-  unfolding permute_fun_def [where f=f]
-  by (simp add: image_image)
-
 lemma finite_permute_iff:
   shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
   unfolding permute_set_eq_vimage

--- a/Nominal/NewFv.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal/NewFv.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -233,12 +233,13 @@
   val fv_nums = 0 upto (length fv_frees - 1)
 
   val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums);
-  val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
-  val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)
+  
+  val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
+  val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
 
   val lthy' =
     lthy
-    |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config
+    |> Function.add_function all_fv_names all_fv_eqs Function_Common.default_config
     |> by_pat_completeness_auto
     |> Local_Theory.restore
     |> termination_by (Lexicographic_Order.lexicographic_order)

--- a/Nominal/NewParser.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal/NewParser.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -1,5 +1,5 @@
 theory NewParser
-imports "../Nominal-General/Nominal2_Atoms" 
+imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
         "Perm" "NewFv"
@@ -449,9 +449,22 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
-
+atom_decl name
 
-atom_decl name
+nominal_datatype lam =
+  Var name
+| App lam lam
+| Lam x::name t::lam  bind_set x in t
+| Let p::pt t::lam bind_set "bn p" in t
+and pt =
+  P1 name
+| P2 pt pt
+binder
+ bn::"pt \<Rightarrow> atom set" 
+where
+  "bn (P1 x) = {atom x}"
+| "bn (P2 p1 p2) = bn p1 \<union> bn p2"
+
 
 nominal_datatype exp =
   EVar name
@@ -507,10 +520,10 @@
 
 (* some further tests *)
 
-nominal_datatype lam =
-  Var "name"
-| App "lam" "lam list"
-| Lam x::"name" t::"lam" bind x in t
+nominal_datatype lam2 =
+  Var2 "name"
+| App2 "lam2" "lam2 list"
+| Lam2 x::"name" t::"lam2" bind x in t
 
 nominal_datatype ty =
   Var "name"

--- a/Nominal/Perm.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal/Perm.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -12,7 +12,8 @@
 *}
 
 ML {*
-(* generates for every datatype a name str ^ dt_name *)
+(* generates for every datatype a name str ^ dt_name 
+   plus and index for multiple occurences of a string *)
 fun prefix_dt_names dt_descr sorts str = 
 let
   fun get_nth_name (i, _) =