--- a/Nominal/Ex/Lambda.thy	Fri Apr 19 00:10:52 2013 +0100
+++ b/Nominal/Ex/Lambda.thy	Tue Jun 04 09:39:23 2013 +0100
@@ -4,6 +4,11 @@
   "~~/src/HOL/Library/Monad_Syntax"
 begin
 
+lemma perm_commute: 
+  "a \<sharp> p \<Longrightarrow> a' \<sharp> p \<Longrightarrow> (a \<rightleftharpoons> a') + p = p + (a \<rightleftharpoons> a')"
+apply(rule plus_perm_eq)
+apply(simp add: supp_swap fresh_def)
+done
 
 atom_decl name
 
@@ -14,6 +19,8 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
+thm lam.strong_induct
+
 lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)"
   unfolding alpha_lam_raw_def
   by perm_simp rule
@@ -378,6 +385,8 @@
   avoids b4: "x"
   by (simp_all add: fresh_star_def fresh_Pair  fresh_fact)
 
+thm beta.strong_induct
+
 text {* One-Reduction *}
 
 inductive 

--- a/Nominal/Nominal2_Base.thy	Fri Apr 19 00:10:52 2013 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 04 09:39:23 2013 +0100
@@ -354,7 +354,6 @@
   unfolding permute_atom_def
   by (metis Rep_perm_ext ext)
 
-
 subsection {* Permutations for permutations *}
 
 instantiation perm :: pt
@@ -1001,6 +1000,11 @@
   shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
   unfolding Un_def by simp
 
+lemma UNION_eqvt [eqvt]:
+  shows "p \<bullet> (UNION A f) = (UNION (p \<bullet> A) (p \<bullet> f))"
+unfolding UNION_eq
+by (perm_simp) (simp)
+
 lemma Diff_eqvt [eqvt]:
   fixes A B :: "'a::pt set"
   shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
@@ -1603,6 +1607,17 @@
     by blast
 qed
 
+lemma perm_eq_iff2:
+  fixes p q :: "perm"
+  shows "p = q \<longleftrightarrow> (\<forall>a::atom \<in> supp p \<union> supp q. p \<bullet> a = q \<bullet> a)"
+  unfolding perm_eq_iff
+  apply(auto)
+  apply(case_tac "a \<sharp> p \<and> a \<sharp> q")
+  apply(simp add: fresh_perm)
+  apply(simp add: fresh_def)
+  done
+
+
 instance perm :: fs
 by default (simp add: supp_perm finite_perm_lemma)
 
@@ -2017,15 +2032,13 @@
   assumes fin: "finite S"
   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 proof -
-  have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" 
-    unfolding eqvt_def 
-    by (perm_simp) (simp)
+  have eqvt: "eqvt (\<lambda>S. \<Union>x \<in> S. supp x)" 
+    unfolding eqvt_def by simp 
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
     by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
-  also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp
   also have "\<dots> \<subseteq> supp S" using eqvt
     by (rule supp_fun_app_eqvt)
-  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
+  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .  
 qed
 
 lemma supp_of_finite_sets:

--- a/Nominal/nominal_function_core.ML	Fri Apr 19 00:10:52 2013 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jun 04 09:39:23 2013 +0100
@@ -501,8 +501,9 @@
       map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems
 
     fun elim_implies_eta A AB =
-      Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
- 
+      Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
+      |> Seq.list_of |> the_single
+
     val uniqueness = G_cases
       |> Thm.forall_elim (cterm_of thy lhs)
       |> Thm.forall_elim (cterm_of thy y)

--- a/Nominal/nominal_mutual.ML	Fri Apr 19 00:10:52 2013 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jun 04 09:39:23 2013 +0100
@@ -418,10 +418,6 @@
 
     val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy'') = define_projections fixes mutual fsum lthy'
 
-    val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
-
-    (* XXX *)
-
     (* defining the auxiliary graph *)
     fun mk_cases (MutualPart {i', fvar as (n, T), ...}) =
       let
@@ -446,6 +442,8 @@
     val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = 
       Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy''
 
+    val mutual_cont = mk_partial_rules_mutual lthy''' cont mutual'
+
     (* proof of equivalence between graph and auxiliary graph *)
     val x = Var(("x", 0), ST)
     val y = Var(("y", 1), RST)