# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1458421608 0
# Node ID c4f31f1564b71f6d08376c8179396640a25646cb
# Parent  4af8a92396cedbe4dd46cc5f8e6d9849e7e58c33
updated to Isabelle 2016

diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Ex/Lambda.thy	Sat Mar 19 21:06:48 2016 +0000
@@ -72,23 +72,6 @@
 unfolding Ident_def
 by simp
 
-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
-
-lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"
-proof -
-  have "alpha_lam_raw (rep_lam (abs_lam t)) t"
-    using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis
-  then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"
-    unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .
-  then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"
-    using Quotient3_rel Quotient3_lam by metis
-  thus ?thesis using permute_lam_def id_apply map_fun_apply by metis
-qed
-
 
 section {* Simple examples from Norrish 2004 *}
 
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Ex/Pi.thy	Sat Mar 19 21:06:48 2016 +0000
@@ -1,571 +1,555 @@
-(* Theory be Kirstin Peters *)
-
-theory Pi
-  imports "../Nominal2"
-begin
-
-atom_decl name
-
-subsection {* Capture-Avoiding Substitution of Names *}
-
-definition
-  subst_name :: "name \<Rightarrow> name \<Rightarrow> name \<Rightarrow> name" ("_[_:::=_]" [110, 110, 110] 110)
-where
-  "a[b:::=c] \<equiv> if (a = b) then c else a"
-
-declare subst_name_def[simp]
-
-lemma subst_name_mix_eqvt[eqvt]:
-  fixes p :: perm
-  and   a :: name
-  and   b :: name
-  and   c :: name
-
-  shows "p \<bullet> (a[b:::=c]) = (p \<bullet> a)[(p \<bullet> b):::=(p \<bullet> c)]"
-proof -
-  show ?thesis
-    by(auto)
-qed
-
-nominal_function
-  subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"
-where
-  "subst_name_list a [] = a"
-| "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"
-  apply(simp add: eqvt_def subst_name_list_graph_aux_def)
-  apply(simp)
-  apply(auto)
-  apply(rule_tac y="b" in list.exhaust)
-  by(auto)
-
-nominal_termination (eqvt)
-  by (lexicographic_order)
-
-
-section {* The Synchronous Pi-Calculus *}
-
-subsection {* Syntax: Synchronous, Monadic Pi-Calculus with n-ary, Mixed Choice *}
-
-nominal_datatype
-      guardedTerm_mix = Output name name piMix                     ("_!<_>\<onesuperior>._" [120, 120, 110] 110)
-                      | Input name b::name P::piMix  binds b in P  ("_?<_>\<onesuperior>._" [120, 120, 110] 110)
-                      | Tau piMix                                  ("<\<tau>\<onesuperior>>._" [110] 110)
-  and sumList_mix     = SumNil                                     ("\<zero>\<onesuperior>")
-                      | AddSummand guardedTerm_mix sumList_mix     (infixr "\<oplus>\<onesuperior>" 65)
-  and piMix           = Res a::name P::piMix         binds a in P  ("<\<nu>_>\<onesuperior>_" [100, 100] 100)
-                      | Par piMix piMix                            (infixr "\<parallel>\<onesuperior>" 85)
-                      | Match name name piMix                      ("[_\<frown>\<onesuperior>_]_" [120, 120, 110] 110)
-                      | Sum sumList_mix                            ("\<oplus>\<onesuperior>{_}" 90)
-                      | Rep name b::name P::piMix    binds b in P  ("\<infinity>_?<_>\<onesuperior>._" [120, 120, 110] 110)
-                      | Succ                                       ("succ\<onesuperior>")
-
-lemmas piMix_strong_induct  = guardedTerm_mix_sumList_mix_piMix.strong_induct
-lemmas piMix_fresh          = guardedTerm_mix_sumList_mix_piMix.fresh
-lemmas piMix_eq_iff         = guardedTerm_mix_sumList_mix_piMix.eq_iff
-lemmas piMix_distinct       = guardedTerm_mix_sumList_mix_piMix.distinct
-lemmas piMix_size           = guardedTerm_mix_sumList_mix_piMix.size
-
-subsection {* Alpha-Conversion Lemmata *}
-
-lemma alphaRes_mix:
-  fixes a :: name
-  and   P :: piMix
-  and   z :: name
-
-  assumes "atom z \<sharp> P"
-
-  shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>((atom a \<rightleftharpoons> atom z) \<bullet> P)"
-proof(cases "a = z")
-  assume "a = z"
-  thus ?thesis
-    by(simp)
-next
-  assume "a \<noteq> z"
-  thus ?thesis
-    using assms
-    by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
-qed
-
-lemma alphaInput_mix:
-  fixes a :: name
-  and   b :: name
-  and   P :: piMix
-  and   z :: name
-
-  assumes "atom z \<sharp> P"
-
-  shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
-proof(cases "b = z")
-  assume "b = z"
-  thus ?thesis
-    by(simp)
-next
-  assume "b \<noteq> z"
-  thus ?thesis
-    using assms
-    by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
-qed
-
-lemma alphaRep_mix:
-  fixes a :: name
-  and   b :: name
-  and   P :: piMix
-  and   z :: name
-
-  assumes "atom z \<sharp> P"
-
-  shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
-proof(cases "b = z")
-  assume "b = z"
-  thus ?thesis
-    by(simp)
-next
-  assume "b \<noteq> z"
-  thus ?thesis
-    using assms
-    by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
-qed
-
-subsection {* Capture-Avoiding Substitution of Names *}
-
-lemma testl:
-  assumes a: "\<exists>y. f = Inl y"
-  shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
-using a by auto
-
-lemma testrr:
-  assumes a: "\<exists>y. f = Inr (Inr y)"
-  shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))"
-using a by auto
-
-lemma testlr:
-  assumes a: "\<exists>y. f = Inr (Inl y)"
-  shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
-using a by auto
-
-nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
-  subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix"  ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
-  subsList_mix  :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix"          ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
-  subs_mix      :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix"                      ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
-where
-  "(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])"
-| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (a?<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
-| "(<\<tau>\<onesuperior>>.P)[x::=\<onesuperior>\<onesuperior>y] = <\<tau>\<onesuperior>>.(P[x::=\<onesuperior>y])"
-| "(\<zero>\<onesuperior>)[x::=\<onesuperior>\<twosuperior>y] = \<zero>\<onesuperior>"
-| "(g \<oplus>\<onesuperior> xg)[x::=\<onesuperior>\<twosuperior>y] = (g[x::=\<onesuperior>\<onesuperior>y]) \<oplus>\<onesuperior> (xg[x::=\<onesuperior>\<twosuperior>y])"
-| "\<lbrakk>atom a \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (<\<nu>a>\<onesuperior>P)[x::=\<onesuperior>y] = <\<nu>a>\<onesuperior>(P[x::=\<onesuperior>y])"
-| "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"
-| "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"
-| "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"
-| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
-| "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
-  using [[simproc del: alpha_lst]]
-  apply(auto simp add: piMix_distinct piMix_eq_iff)
-  apply(simp add: eqvt_def  subsGuard_mix_subsList_mix_subs_mix_graph_aux_def)
-  --"Covered all cases"
-  apply(case_tac x)
-  apply(simp)
-  apply(case_tac a)
-  apply(simp)
-  apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1))
-  apply(blast)
-  apply(auto simp add: fresh_star_def)[1]
-  apply(blast)
-  apply(simp)
-  apply(case_tac b)
-  apply(simp)
-  apply(case_tac a)
-  apply(simp)
-  apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2))
-  apply(blast)
-  apply(blast)
-  apply(simp)
-  apply(case_tac ba)
-  apply(simp)
-  apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))
-  using [[simproc del: alpha_lst]]
-  apply(auto simp add: fresh_star_def)[1]
-  apply(blast)
-  apply(blast)
-  apply(blast)
-  using [[simproc del: alpha_lst]]
-  apply(auto simp add: fresh_star_def)[1]
-  apply(simp)
-  --"compatibility"
-  apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
-  apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
-  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
-  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
-  prefer 2
-  apply (simp only: eqvt_at_def subs_mix_def)
-  apply rule
-  apply(simp (no_asm))
-  apply (subst testrr)
-  apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
-  apply (simp add: THE_default_def)
-apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
-apply simp_all[2]
-apply auto[1]
-apply (erule_tac x="x" in allE)
-apply simp
-apply (thin_tac "\<forall>p\<Colon>perm.
-           p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
-           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
-            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
-            else Inr (Inr undefined))")
-apply (thin_tac "\<forall>p\<Colon>perm.
-           p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                      subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
-                then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                        subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
-                else Inr (Inr undefined)) =
-           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
-            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
-            else Inr (Inr undefined))")
-apply (thin_tac "atom b \<sharp> (xa, ya)")
-apply (thin_tac "atom ba \<sharp> (xa, ya)")
-apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
-apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-apply assumption
-apply (metis Inr_not_Inl)
-apply (metis Inr_not_Inl)
-apply (metis Inr_not_Inl)
-apply (metis Inr_inject Inr_not_Inl)
-apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
-                            (Sum_Type.projr
-                              (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="Sum_Type.projr
-                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
-                      Sum_Type.projr
-                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
-                                                    (Sum_Type.projr
-(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
-                          (Sum_Type.projr
-                            (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
-                                           (Sum_Type.projr
-                                             (subsGuard_mix_subsList_mix_subs_mix_sum
-                                               (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="succ\<onesuperior>" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply simp
-(* Here the only real goal compatibility is left *)
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
-  apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
-  apply simp
-  apply (erule fresh_eqvt_at)
-  apply(simp add: finite_supp)
-  apply(simp)
-  apply(simp add: eqvt_at_def)
-  apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
-  apply(simp)
-  apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
-  apply(rename_tac b P ba xa ya Pa)
- apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
-  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
-  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
-  prefer 2
-  apply (simp only: eqvt_at_def subs_mix_def)
-  apply rule
-  apply(simp (no_asm))
-  apply (subst testrr)
-  apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
-  apply (simp add: THE_default_def)
-apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
-apply simp_all[2]
-apply auto[1]
-apply (erule_tac x="x" in allE)
-apply simp
-apply (thin_tac "\<forall>p\<Colon>perm.
-           p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
-           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
-            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
-            else Inr (Inr undefined))")
-apply (thin_tac "\<forall>p\<Colon>perm.
-           p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                      subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
-                then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                        subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
-                else Inr (Inr undefined)) =
-           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
-            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.
-                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
-            else Inr (Inr undefined))")
-apply (thin_tac "atom b \<sharp> (xa, ya)")
-apply (thin_tac "atom ba \<sharp> (xa, ya)")
-apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
-apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
-apply assumption
-apply (metis Inr_not_Inl)
-apply (metis Inr_not_Inl)
-apply (metis Inr_not_Inl)
-apply (metis Inr_inject Inr_not_Inl)
-apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
-                            (Sum_Type.projr
-                              (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="Sum_Type.projr
-                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
-                      Sum_Type.projr
-                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
-                                                    (Sum_Type.projr
-(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
-                          (Sum_Type.projr
-                            (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
-                                           (Sum_Type.projr
-                                             (subsGuard_mix_subsList_mix_subs_mix_sum
-                                               (Inr (Inr (Pb, xb, y)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="succ\<onesuperior>" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply simp
-(* Here the only real goal compatibility is left *)
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
-  apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
-  apply simp
-  apply (erule fresh_eqvt_at)
-  apply(simp add: finite_supp)
-  apply(simp)
-  apply(simp add: eqvt_at_def)
-  apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
-  apply(simp)
-  done
-
-nominal_termination (eqvt)
-  by (lexicographic_order)
-
-lemma forget_mix:
-  fixes g  :: guardedTerm_mix
-  and   xg :: sumList_mix
-  and   P  :: piMix
-  and   x  :: name
-  and   y  :: name
-
-  shows "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
-  and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
-  and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
-proof -
-  show  "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
-  and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
-  and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
-    using assms
-    apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
-    by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)
-qed
-
-lemma fresh_fact_mix:
-  fixes g  :: guardedTerm_mix
-  and   xg :: sumList_mix
-  and   P  :: piMix
-  and   x  :: name
-  and   y  :: name
-  and   z  :: name
-
-  assumes "atom z \<sharp> y"
-
-  shows "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
-  and   "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
-  and   "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
-proof -
-  show  "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
-  and   "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
-  and   "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
-    using assms
-    apply(nominal_induct g and xg and P avoiding: x y z rule: piMix_strong_induct)
-    by(auto simp add: piMix_fresh fresh_at_base)
-qed
-
-lemma substitution_lemma_mix:
-  fixes g  :: guardedTerm_mix
-  and   xg :: sumList_mix
-  and   P  :: piMix
-  and   s  :: name
-  and   u  :: name
-  and   x  :: name
-  and   y  :: name
-
-  assumes "x \<noteq> y"
-  and     "atom x \<sharp> u"
-
-  shows "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
-  and   "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
-  and   "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
-proof -
-  show  "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
-  and   "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
-  and   "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
-    using assms
-    apply(nominal_induct g and xg and P avoiding: x y s u rule: piMix_strong_induct)
-    apply(simp_all add: fresh_fact_mix forget_mix)
-    by(auto simp add: fresh_at_base)
-qed
-
-lemma perm_eq_subst_mix:
-  fixes g  :: guardedTerm_mix
-  and   xg :: sumList_mix
-  and   P  :: piMix
-  and   x  :: name
-  and   y  :: name
-
-  shows "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
-  and   "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
-  and   "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
-proof -
-  show  "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
-  and   "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
-  and   "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
-    apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
-    by(auto simp add: piMix_fresh fresh_at_base)
-qed
-
-lemma subst_id_mix:
-  fixes g  :: guardedTerm_mix
-  and   xg :: sumList_mix
-  and   P  :: piMix
-  and   x  :: name
-
-  shows "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
-proof -
-  show  "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
-    apply(nominal_induct g and xg and P avoiding: x rule: piMix_strong_induct)
-    by(auto)
-qed
-
-lemma alphaRes_subst_mix:
-  fixes a :: name
-  and   P :: piMix
-  and   z :: name
-
-  assumes "atom z \<sharp> P"
-
-  shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>(P[a::=\<onesuperior>z])"
-proof(cases "a = z")
-  assume "a = z"
-  thus ?thesis
-    by(simp add: subst_id_mix)
-next
-  assume "a \<noteq> z"
-  thus ?thesis
-    using assms
-    by(simp add: alphaRes_mix perm_eq_subst_mix)
-qed
-
-lemma alphaInput_subst_mix:
-  fixes a :: name
-  and   b :: name
-  and   P :: piMix
-  and   z :: name
-
-  assumes "atom z \<sharp> P"
-
-  shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
-proof(cases "b = z")
-  assume "b = z"
-  thus ?thesis
-    by(simp add: subst_id_mix)
-next
-  assume "b \<noteq> z"
-  thus ?thesis
-    using assms
-    by(simp add: alphaInput_mix perm_eq_subst_mix)
-qed
-
-lemma alphaRep_subst_mix:
-  fixes a :: name
-  and   b :: name
-  and   P :: piMix
-  and   z :: name
-
-  assumes "atom z \<sharp> P"
-
-  shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
-proof(cases "b = z")
-  assume "b = z"
-  thus ?thesis
-    by(simp add: subst_id_mix)
-next
-  assume "b \<noteq> z"
-  thus ?thesis
-    using assms
-    by(simp add: alphaRep_mix perm_eq_subst_mix)
-qed
-
-inductive
-  fresh_list_guard_mix :: "name list \<Rightarrow> guardedTerm_mix \<Rightarrow> bool"
-where
-  "fresh_list_guard_mix [] g"
-| "\<lbrakk>atom n \<sharp> g; fresh_list_guard_mix xn g\<rbrakk> \<Longrightarrow> fresh_list_guard_mix (n#xn) g"
-
-equivariance fresh_list_guard_mix
-nominal_inductive fresh_list_guard_mix
-  done
-
-inductive
-  fresh_list_sumList_mix :: "name list \<Rightarrow> sumList_mix \<Rightarrow> bool"
-where
-  "fresh_list_sumList_mix [] xg"
-| "\<lbrakk>atom n \<sharp> xg; fresh_list_sumList_mix xn xg\<rbrakk> \<Longrightarrow> fresh_list_sumList_mix (n#xn) xg"
-
-equivariance fresh_list_sumList_mix
-nominal_inductive fresh_list_sumList_mix
-  done
-
-inductive
-  fresh_list_mix :: "name list \<Rightarrow> piMix \<Rightarrow> bool"
-where
-  "fresh_list_mix [] P"
-| "\<lbrakk>atom n \<sharp> P; fresh_list_mix xn P\<rbrakk> \<Longrightarrow> fresh_list_mix (n#xn) P"
-
-equivariance fresh_list_mix
-nominal_inductive fresh_list_mix
-  done
-
+(* Theory be Kirstin Peters *)
+
+theory Pi
+  imports "../Nominal2"
+begin
+
+atom_decl name
+
+subsection {* Capture-Avoiding Substitution of Names *}
+
+definition
+  subst_name :: "name \<Rightarrow> name \<Rightarrow> name \<Rightarrow> name" ("_[_:::=_]" [110, 110, 110] 110)
+where
+  "a[b:::=c] \<equiv> if (a = b) then c else a"
+
+declare subst_name_def[simp]
+
+lemma subst_name_mix_eqvt[eqvt]:
+  fixes p :: perm
+  and   a :: name
+  and   b :: name
+  and   c :: name
+
+  shows "p \<bullet> (a[b:::=c]) = (p \<bullet> a)[(p \<bullet> b):::=(p \<bullet> c)]"
+proof -
+  show ?thesis
+    by(auto)
+qed
+
+nominal_function
+  subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"
+where
+  "subst_name_list a [] = a"
+| "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"
+  apply(simp add: eqvt_def subst_name_list_graph_aux_def)
+  apply(simp)
+  apply(auto)
+  apply(rule_tac y="b" in list.exhaust)
+  by(auto)
+
+nominal_termination (eqvt)
+  by (lexicographic_order)
+
+
+section {* The Synchronous Pi-Calculus *}
+
+subsection {* Syntax: Synchronous, Monadic Pi-Calculus with n-ary, Mixed Choice *}
+
+nominal_datatype
+      guardedTerm_mix = Output name name piMix                     ("_!<_>\<onesuperior>._" [120, 120, 110] 110)
+                      | Input name b::name P::piMix  binds b in P  ("_?<_>\<onesuperior>._" [120, 120, 110] 110)
+                      | Tau piMix                                  ("<\<tau>\<onesuperior>>._" [110] 110)
+  and sumList_mix     = SumNil                                     ("\<zero>\<onesuperior>")
+                      | AddSummand guardedTerm_mix sumList_mix     (infixr "\<oplus>\<onesuperior>" 65)
+  and piMix           = Res a::name P::piMix         binds a in P  ("<\<nu>_>\<onesuperior>_" [100, 100] 100)
+                      | Par piMix piMix                            (infixr "\<parallel>\<onesuperior>" 85)
+                      | Match name name piMix                      ("[_\<frown>\<onesuperior>_]_" [120, 120, 110] 110)
+                      | Sum sumList_mix                            ("\<oplus>\<onesuperior>{_}" 90)
+                      | Rep name b::name P::piMix    binds b in P  ("\<infinity>_?<_>\<onesuperior>._" [120, 120, 110] 110)
+                      | Succ                                       ("succ\<onesuperior>")
+
+lemmas piMix_strong_induct  = guardedTerm_mix_sumList_mix_piMix.strong_induct
+lemmas piMix_fresh          = guardedTerm_mix_sumList_mix_piMix.fresh
+lemmas piMix_eq_iff         = guardedTerm_mix_sumList_mix_piMix.eq_iff
+lemmas piMix_distinct       = guardedTerm_mix_sumList_mix_piMix.distinct
+lemmas piMix_size           = guardedTerm_mix_sumList_mix_piMix.size
+
+subsection {* Alpha-Conversion Lemmata *}
+
+lemma alphaRes_mix:
+  fixes a :: name
+  and   P :: piMix
+  and   z :: name
+
+  assumes "atom z \<sharp> P"
+
+  shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>((atom a \<rightleftharpoons> atom z) \<bullet> P)"
+proof(cases "a = z")
+  assume "a = z"
+  thus ?thesis
+    by(simp)
+next
+  assume "a \<noteq> z"
+  thus ?thesis
+    using assms
+    by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+qed
+
+lemma alphaInput_mix:
+  fixes a :: name
+  and   b :: name
+  and   P :: piMix
+  and   z :: name
+
+  assumes "atom z \<sharp> P"
+
+  shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
+proof(cases "b = z")
+  assume "b = z"
+  thus ?thesis
+    by(simp)
+next
+  assume "b \<noteq> z"
+  thus ?thesis
+    using assms
+    by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+qed
+
+lemma alphaRep_mix:
+  fixes a :: name
+  and   b :: name
+  and   P :: piMix
+  and   z :: name
+
+  assumes "atom z \<sharp> P"
+
+  shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"
+proof(cases "b = z")
+  assume "b = z"
+  thus ?thesis
+    by(simp)
+next
+  assume "b \<noteq> z"
+  thus ?thesis
+    using assms
+    by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+qed
+
+subsection {* Capture-Avoiding Substitution of Names *}
+
+lemma testl:
+  assumes a: "\<exists>y. f = Inl y"
+  shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
+using a by auto
+
+lemma testrr:
+  assumes a: "\<exists>y. f = Inr (Inr y)"
+  shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))"
+using a by auto
+
+lemma testlr:
+  assumes a: "\<exists>y. f = Inr (Inl y)"
+  shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
+using a by auto
+
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+  subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix"  ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
+  subsList_mix  :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix"          ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
+  subs_mix      :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix"                      ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
+where
+  "(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])"
+| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (a?<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
+| "(<\<tau>\<onesuperior>>.P)[x::=\<onesuperior>\<onesuperior>y] = <\<tau>\<onesuperior>>.(P[x::=\<onesuperior>y])"
+| "(\<zero>\<onesuperior>)[x::=\<onesuperior>\<twosuperior>y] = \<zero>\<onesuperior>"
+| "(g \<oplus>\<onesuperior> xg)[x::=\<onesuperior>\<twosuperior>y] = (g[x::=\<onesuperior>\<onesuperior>y]) \<oplus>\<onesuperior> (xg[x::=\<onesuperior>\<twosuperior>y])"
+| "\<lbrakk>atom a \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (<\<nu>a>\<onesuperior>P)[x::=\<onesuperior>y] = <\<nu>a>\<onesuperior>(P[x::=\<onesuperior>y])"
+| "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"
+| "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"
+| "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"
+| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
+| "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
+  using [[simproc del: alpha_lst]]
+  apply(auto simp add: piMix_distinct piMix_eq_iff)
+  apply(simp add: eqvt_def  subsGuard_mix_subsList_mix_subs_mix_graph_aux_def)
+  --"Covered all cases"
+  apply(case_tac x)
+  apply(simp)
+  apply(case_tac a)
+  apply(simp)
+  apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1))
+  apply(blast)
+  apply(auto simp add: fresh_star_def)[1]
+  apply(blast)
+  apply(simp)
+  apply(case_tac b)
+  apply(simp)
+  apply(case_tac a)
+  apply(simp)
+  apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2))
+  apply(blast)
+  apply(blast)
+  apply(simp)
+  apply(case_tac ba)
+  apply(simp)
+  apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))
+  using [[simproc del: alpha_lst]]
+  apply(auto simp add: fresh_star_def)[1]
+  apply(blast)
+  apply(blast)
+  apply(blast)
+  using [[simproc del: alpha_lst]]
+  apply(auto simp add: fresh_star_def)[1]
+  apply(simp)
+  --"compatibility"
+  apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
+  apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
+  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
+  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
+  prefer 2
+  apply (simp only: eqvt_at_def subs_mix_def)
+  apply rule
+  apply(simp (no_asm))
+  apply (subst testrr)
+  apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
+  apply (simp add: THE_default_def)
+apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
+apply simp_all[2]
+apply auto[1]
+apply (erule_tac x="x" in allE)
+apply simp
+apply(thin_tac "\<forall>p. p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
+            (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+             then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+             else Inr (Inr undefined))")
+apply(thin_tac "\<forall>p. p \<bullet> (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+                 then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+                 else Inr (Inr undefined)) =
+            (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+             then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+             else Inr (Inr undefined))")
+apply (thin_tac "atom b \<sharp> (xa, ya)")
+apply (thin_tac "atom ba \<sharp> (xa, ya)")
+apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
+apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
+apply assumption
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+                            (Sum_Type.projr
+                              (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="Sum_Type.projr
+                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+                      Sum_Type.projr
+                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+                                                    (Sum_Type.projr
+(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+                          (Sum_Type.projr
+                            (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+                                           (Sum_Type.projr
+                                             (subsGuard_mix_subsList_mix_subs_mix_sum
+                                               (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="succ\<onesuperior>" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply simp
+(* Here the only real goal compatibility is left *)
+  apply (erule Abs_lst1_fcb)
+  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
+  apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
+  apply simp
+  apply (erule fresh_eqvt_at)
+  apply(simp add: finite_supp)
+  apply(simp)
+  apply(simp add: eqvt_at_def)
+  apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
+  apply(simp)
+  apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
+  apply(rename_tac b P ba xa ya Pa)
+ apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")
+  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")
+  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")
+  prefer 2
+  apply (simp only: eqvt_at_def subs_mix_def)
+  apply rule
+  apply(simp (no_asm))
+  apply (subst testrr)
+  apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)
+  apply (simp add: THE_default_def)
+apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")
+apply simp_all[2]
+apply auto[1]
+apply (erule_tac x="x" in allE)
+apply simp
+apply(thin_tac "\<forall>p. p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =
+            (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+             then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x
+             else Inr (Inr undefined))")
+apply(thin_tac "\<forall>p. p \<bullet> (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+                 then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x
+                 else Inr (Inr undefined)) =
+            (if \<exists>!x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+             then THE x. subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x
+             else Inr (Inr undefined))")
+apply (thin_tac "atom b \<sharp> (xa, ya)")
+apply (thin_tac "atom ba \<sharp> (xa, ya)")
+apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")
+apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)
+apply assumption
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (metis Inr_inject Inr_not_Inl)
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+                            (Sum_Type.projr
+                              (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="Sum_Type.projr
+                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+                      Sum_Type.projr
+                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+                                                    (Sum_Type.projr
+(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+                          (Sum_Type.projr
+                            (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+                                           (Sum_Type.projr
+                                             (subsGuard_mix_subsList_mix_subs_mix_sum
+                                               (Inr (Inr (Pb, xb, y)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply (rule_tac x="succ\<onesuperior>" in exI)
+apply clarify
+apply (rule the1_equality)
+apply blast apply assumption
+apply simp
+(* Here the only real goal compatibility is left *)
+  apply (erule Abs_lst1_fcb)
+  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
+  apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")
+  apply simp
+  apply (erule fresh_eqvt_at)
+  apply(simp add: finite_supp)
+  apply(simp)
+  apply(simp add: eqvt_at_def)
+  apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
+  apply(simp)
+  done
+
+nominal_termination (eqvt)
+  by (lexicographic_order)
+
+lemma forget_mix:
+  fixes g  :: guardedTerm_mix
+  and   xg :: sumList_mix
+  and   P  :: piMix
+  and   x  :: name
+  and   y  :: name
+
+  shows "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
+  and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
+  and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
+proof -
+  show  "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
+  and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
+  and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
+    using assms
+    apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
+    by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)
+qed
+
+lemma fresh_fact_mix:
+  fixes g  :: guardedTerm_mix
+  and   xg :: sumList_mix
+  and   P  :: piMix
+  and   x  :: name
+  and   y  :: name
+  and   z  :: name
+
+  assumes "atom z \<sharp> y"
+
+  shows "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
+  and   "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
+  and   "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
+proof -
+  show  "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"
+  and   "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"
+  and   "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"
+    using assms
+    apply(nominal_induct g and xg and P avoiding: x y z rule: piMix_strong_induct)
+    by(auto simp add: piMix_fresh fresh_at_base)
+qed
+
+lemma substitution_lemma_mix:
+  fixes g  :: guardedTerm_mix
+  and   xg :: sumList_mix
+  and   P  :: piMix
+  and   s  :: name
+  and   u  :: name
+  and   x  :: name
+  and   y  :: name
+
+  assumes "x \<noteq> y"
+  and     "atom x \<sharp> u"
+
+  shows "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
+  and   "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
+  and   "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
+proof -
+  show  "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"
+  and   "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"
+  and   "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"
+    using assms
+    apply(nominal_induct g and xg and P avoiding: x y s u rule: piMix_strong_induct)
+    apply(simp_all add: fresh_fact_mix forget_mix)
+    by(auto simp add: fresh_at_base)
+qed
+
+lemma perm_eq_subst_mix:
+  fixes g  :: guardedTerm_mix
+  and   xg :: sumList_mix
+  and   P  :: piMix
+  and   x  :: name
+  and   y  :: name
+
+  shows "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
+  and   "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
+  and   "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
+proof -
+  show  "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"
+  and   "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"
+  and   "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"
+    apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
+    by(auto simp add: piMix_fresh fresh_at_base)
+qed
+
+lemma subst_id_mix:
+  fixes g  :: guardedTerm_mix
+  and   xg :: sumList_mix
+  and   P  :: piMix
+  and   x  :: name
+
+  shows "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
+proof -
+  show  "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"
+    apply(nominal_induct g and xg and P avoiding: x rule: piMix_strong_induct)
+    by(auto)
+qed
+
+lemma alphaRes_subst_mix:
+  fixes a :: name
+  and   P :: piMix
+  and   z :: name
+
+  assumes "atom z \<sharp> P"
+
+  shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>(P[a::=\<onesuperior>z])"
+proof(cases "a = z")
+  assume "a = z"
+  thus ?thesis
+    by(simp add: subst_id_mix)
+next
+  assume "a \<noteq> z"
+  thus ?thesis
+    using assms
+    by(simp add: alphaRes_mix perm_eq_subst_mix)
+qed
+
+lemma alphaInput_subst_mix:
+  fixes a :: name
+  and   b :: name
+  and   P :: piMix
+  and   z :: name
+
+  assumes "atom z \<sharp> P"
+
+  shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
+proof(cases "b = z")
+  assume "b = z"
+  thus ?thesis
+    by(simp add: subst_id_mix)
+next
+  assume "b \<noteq> z"
+  thus ?thesis
+    using assms
+    by(simp add: alphaInput_mix perm_eq_subst_mix)
+qed
+
+lemma alphaRep_subst_mix:
+  fixes a :: name
+  and   b :: name
+  and   P :: piMix
+  and   z :: name
+
+  assumes "atom z \<sharp> P"
+
+  shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"
+proof(cases "b = z")
+  assume "b = z"
+  thus ?thesis
+    by(simp add: subst_id_mix)
+next
+  assume "b \<noteq> z"
+  thus ?thesis
+    using assms
+    by(simp add: alphaRep_mix perm_eq_subst_mix)
+qed
+
+inductive
+  fresh_list_guard_mix :: "name list \<Rightarrow> guardedTerm_mix \<Rightarrow> bool"
+where
+  "fresh_list_guard_mix [] g"
+| "\<lbrakk>atom n \<sharp> g; fresh_list_guard_mix xn g\<rbrakk> \<Longrightarrow> fresh_list_guard_mix (n#xn) g"
+
+equivariance fresh_list_guard_mix
+nominal_inductive fresh_list_guard_mix
+  done
+
+inductive
+  fresh_list_sumList_mix :: "name list \<Rightarrow> sumList_mix \<Rightarrow> bool"
+where
+  "fresh_list_sumList_mix [] xg"
+| "\<lbrakk>atom n \<sharp> xg; fresh_list_sumList_mix xn xg\<rbrakk> \<Longrightarrow> fresh_list_sumList_mix (n#xn) xg"
+
+equivariance fresh_list_sumList_mix
+nominal_inductive fresh_list_sumList_mix
+  done
+
+inductive
+  fresh_list_mix :: "name list \<Rightarrow> piMix \<Rightarrow> bool"
+where
+  "fresh_list_mix [] P"
+| "\<lbrakk>atom n \<sharp> P; fresh_list_mix xn P\<rbrakk> \<Longrightarrow> fresh_list_mix (n#xn) P"
+
+equivariance fresh_list_mix
+nominal_inductive fresh_list_mix
+  done
+
 end
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2.thy	Sat Mar 19 21:06:48 2016 +0000
@@ -178,7 +178,7 @@
   val raw_induct_thms = #inducts (hd dtinfos)
   val raw_exhaust_thms = map #exhaust dtinfos
   val raw_size_trms = map HOLogic.size_const raw_tys
-  val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o fst o snd)
+  val raw_size_thms = these (Option.map ((fn ths => drop (length ths div 2) ths) o #2 o #2)
     (BNF_LFP_Size.size_of lthy1 (hd raw_full_dt_names')))
 
   val raw_result = RawDtInfo 
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2_Abs.thy	Sat Mar 19 21:06:48 2016 +0000
@@ -537,7 +537,7 @@
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
-  apply(default)
+  apply standard
   apply(case_tac [!] x)
   apply(simp_all)
   done
@@ -559,7 +559,7 @@
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
-  apply(default)
+  apply standard
   apply(case_tac [!] x)
   apply(simp_all)
   done
@@ -581,7 +581,7 @@
   by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"])
 
 instance
-  apply(default)
+  apply standard
   apply(case_tac [!] x)
   apply(simp_all)
   done
@@ -700,19 +700,19 @@
 by (simp_all add: Abs_finite_supp finite_supp)
 
 instance abs_set :: (fs) fs
-  apply(default)
+  apply standard
   apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_res :: (fs) fs
-  apply(default)
+  apply standard
   apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_lst :: (fs) fs
-  apply(default)
+  apply standard
   apply(case_tac x)
   apply(simp add: supp_Abs finite_supp)
   done
@@ -933,7 +933,7 @@
       |> Thm.cterm_of ctxt
     val cvrs_ty = Thm.ctyp_of_cterm cvrs
     val thm' = thm
-      |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] 
+      |> Thm.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] 
   in
     SOME thm'
   end
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2_Base.thy	Sat Mar 19 21:06:48 2016 +0000
@@ -13,6 +13,9 @@
   "atom_decl" "equivariance" :: thy_decl 
 begin
 
+declare [[typedef_overloaded]]
+
+
 section {* Atoms and Sorts *}
 
 text {* A simple implementation for atom_sorts is strings. *}
@@ -183,7 +186,7 @@
   by (simp add: Abs_perm_inverse perm_inv Rep_perm)
 
 instance
-apply default
+apply standard
 unfolding Rep_perm_inject [symmetric]
 unfolding minus_perm_def
 unfolding Rep_perm_add
@@ -325,7 +328,7 @@
   "p \<bullet> a = (Rep_perm p) a"
 
 instance 
-apply(default)
+apply standard
 apply(simp_all add: permute_atom_def Rep_perm_simps)
 done
 
@@ -363,7 +366,7 @@
   "p \<bullet> q = p + q - p"
 
 instance
-apply default
+apply standard
 apply (simp add: permute_perm_def)
 apply (simp add: permute_perm_def algebra_simps)
 done
@@ -390,7 +393,7 @@
   "p \<bullet> f = (\<lambda>x. p \<bullet> (f (- p \<bullet> x)))"
 
 instance
-apply default
+apply standard
 apply (simp add: permute_fun_def)
 apply (simp add: permute_fun_def minus_add)
 done
@@ -413,7 +416,7 @@
 definition "p \<bullet> (b::bool) = b"
 
 instance
-apply(default) 
+apply standard
 apply(simp_all add: permute_bool_def)
 done
 
@@ -438,7 +441,7 @@
   "p \<bullet> X = {p \<bullet> x | x. x \<in> X}" 
 
 instance
-apply default
+apply standard
 apply (auto simp: permute_set_def)
 done
 
@@ -510,7 +513,7 @@
 definition "p \<bullet> (u::unit) = u"
 
 instance 
-by (default) (simp_all add: permute_unit_def)
+  by standard (simp_all add: permute_unit_def)
 
 end
 
@@ -526,7 +529,7 @@
   Pair_eqvt: "p \<bullet> (x, y) = (p \<bullet> x, p \<bullet> y)"
 
 instance
-by default auto
+  by standard auto
 
 end
 
@@ -542,7 +545,7 @@
 | Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
 
 instance 
-by (default) (case_tac [!] x, simp_all)
+  by standard (case_tac [!] x, simp_all)
 
 end
 
@@ -558,7 +561,7 @@
 | Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
 
 instance 
-by (default) (induct_tac [!] x, simp_all)
+  by standard (induct_tac [!] x, simp_all)
 
 end
 
@@ -580,7 +583,7 @@
 | Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)"
 
 instance 
-by (default) (induct_tac [!] x, simp_all)
+  by standard (induct_tac [!] x, simp_all)
 
 end
 
@@ -667,7 +670,7 @@
   done
 
 instance
-apply(default)
+apply standard
 apply(transfer)
 apply(simp)
 apply(transfer)
@@ -685,7 +688,7 @@
 definition "p \<bullet> (c::char) = c"
 
 instance 
-by (default) (simp_all add: permute_char_def)
+  by standard (simp_all add: permute_char_def)
 
 end
 
@@ -695,7 +698,7 @@
 definition "p \<bullet> (n::nat) = n"
 
 instance 
-by (default) (simp_all add: permute_nat_def)
+  by standard (simp_all add: permute_nat_def)
 
 end
 
@@ -705,7 +708,7 @@
 definition "p \<bullet> (i::int) = i"
 
 instance 
-by (default) (simp_all add: permute_int_def)
+  by standard (simp_all add: permute_int_def)
 
 end
 
@@ -729,22 +732,22 @@
 text {* Other type constructors preserve purity. *}
 
 instance "fun" :: (pure, pure) pure
-by default (simp add: permute_fun_def permute_pure)
+  by standard (simp add: permute_fun_def permute_pure)
 
 instance set :: (pure) pure
-by default (simp add: permute_set_def permute_pure)
+  by standard (simp add: permute_set_def permute_pure)
 
 instance prod :: (pure, pure) pure
-by default (induct_tac x, simp add: permute_pure)
+  by standard (induct_tac x, simp add: permute_pure)
 
 instance sum :: (pure, pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+  by standard (induct_tac x, simp_all add: permute_pure)
 
 instance list :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+  by standard (induct_tac x, simp_all add: permute_pure)
 
 instance option :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+  by standard (induct_tac x, simp_all add: permute_pure)
 
 
 subsection {* Types @{typ char}, @{typ nat}, and @{typ int} *}
@@ -1069,7 +1072,7 @@
 begin
 
 instance 
-apply(default)
+apply standard
 unfolding le_bool_def
 apply(perm_simp)
 apply(rule refl)
@@ -1081,7 +1084,7 @@
 begin
 
 instance 
-apply(default)
+apply standard
 unfolding le_fun_def
 apply(perm_simp)
 apply(rule refl)
@@ -1093,7 +1096,7 @@
 begin
 
 instance 
-apply(default)
+apply standard
 unfolding Inf_bool_def
 apply(perm_simp)
 apply(rule refl)
@@ -1105,7 +1108,7 @@
 begin
 
 instance 
-apply(default)
+apply standard
 unfolding Inf_fun_def INF_def
 apply(perm_simp)
 apply(rule refl)
@@ -1145,7 +1148,7 @@
   by (cases x) simp
 
 lemma split_eqvt [eqvt]: 
-  shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+  shows "p \<bullet> (case_prod P x) = case_prod (p \<bullet> P) (p \<bullet> x)"
   unfolding split_def
   by simp
 
@@ -1456,7 +1459,7 @@
   unfolding fresh_def by (simp add: pure_supp)
 
 instance pure < fs
-by default (simp add: pure_supp)
+  by standard (simp add: pure_supp)
 
 
 subsection  {* Type @{typ atom} is finitely-supported. *}
@@ -1474,7 +1477,7 @@
   unfolding fresh_def supp_atom by simp
 
 instance atom :: fs
-by default (simp add: supp_atom)
+  by standard (simp add: supp_atom)
 
 
 section {* Type @{typ perm} is finitely-supported. *}
@@ -1623,7 +1626,7 @@
 
 
 instance perm :: fs
-by default (simp add: supp_perm finite_perm_lemma)
+  by standard (simp add: supp_perm finite_perm_lemma)
 
 
 
@@ -1649,7 +1652,7 @@
   by (simp add: fresh_def supp_Unit)
 
 instance prod :: (fs, fs) fs
-apply default
+apply standard
 apply (case_tac x)
 apply (simp add: supp_Pair finite_supp)
 done
@@ -1674,7 +1677,7 @@
   by (simp add: fresh_def supp_Inr)
 
 instance sum :: (fs, fs) fs
-apply default
+apply standard
 apply (case_tac x)
 apply (simp_all add: supp_Inl supp_Inr finite_supp)
 done
@@ -1699,7 +1702,7 @@
   by (simp add: fresh_def supp_Some)
 
 instance option :: (fs) fs
-apply default
+apply standard
 apply (induct_tac x)
 apply (simp_all add: supp_None supp_Some finite_supp)
 done
@@ -1752,7 +1755,7 @@
    (simp_all add: supp_Nil supp_Cons supp_atom)
 
 instance list :: (fs) fs
-apply default
+apply standard
 apply (induct_tac x)
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
@@ -1895,7 +1898,7 @@
         val cty_inst =
           [SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))]
         val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)] 
-        val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+        val thm = Thm.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
       in
         SOME(thm RS @{thm Eq_TrueI}) 
       end  
@@ -2120,12 +2123,12 @@
 
 subsection {* Type @{typ "'a multiset"} is finitely supported *}
 
-lemma set_of_eqvt [eqvt]:
-  shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
+lemma set_mset_eqvt [eqvt]:
+  shows "p \<bullet> (set_mset M) = set_mset (p \<bullet> M)"
 by (induct M) (simp_all add: insert_eqvt empty_eqvt)
 
-lemma supp_set_of:
-  shows "supp (set_of M) \<subseteq> supp M"
+lemma supp_set_mset:
+  shows "supp (set_mset M) \<subseteq> supp M"
   apply (rule supp_fun_app_eqvt)
   unfolding eqvt_def
   apply(perm_simp)
@@ -2165,11 +2168,11 @@
   fixes M::"('a::fs multiset)" 
   shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"
 proof -
-  have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
-  also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
-  also have "... = supp (set_of M)"
+  have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_mset M})" by simp
+  also have "... \<subseteq> (\<Union>x \<in> set_mset M. supp x)" by auto
+  also have "... = supp (set_mset M)"
     by (simp add: supp_of_finite_sets)
-  also have " ... \<subseteq> supp M" by (rule supp_set_of)
+  also have " ... \<subseteq> supp M" by (rule supp_set_mset)
   finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
 qed
 
@@ -2199,9 +2202,7 @@
   by simp
 
 instance multiset :: (fs) fs
-  apply (default)
-  apply (rule multisets_supp_finite)
-  done
+  by standard (rule multisets_supp_finite)
 
 subsection {* Type @{typ "'a fset"} is finitely supported *}
 
@@ -2252,9 +2253,7 @@
 by (simp add: supp_union_fset)
 
 instance fset :: (fs) fs
-  apply (default)
-  apply (rule fset_finite_supp)
-  done
+  by standard (rule fset_finite_supp)
 
 
 subsection {* Type @{typ "('a, 'b) finfun"} is finitely supported *}
@@ -2279,7 +2278,7 @@
 by (auto simp: fresh_def supp_Pair)
     
 instance finfun :: (fs, fs) fs
-  apply(default)
+  apply standard
   apply(induct_tac x rule: finfun_weak_induct)
   apply(simp add: supp_finfun_const finite_supp)
   apply(rule finite_subset)
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_atoms.ML
--- a/Nominal/nominal_atoms.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_atoms.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -12,7 +12,7 @@
   val add_atom_decl: (binding * (binding option)) -> theory -> theory
 end;
 
-structure Atom_Decl :> ATOM_DECL =
+structure Atom_Decl : ATOM_DECL =
 struct
 
 val simp_attr = Attrib.internal (K Simplifier.simp_add)
@@ -32,9 +32,9 @@
 
     (* typedef *)
     val set = atom_decl_set str;
-    fun tac _ = rtac @{thm exists_eq_simple_sort} 1;
+    fun tac ctxt = resolve_tac ctxt @{thms exists_eq_simple_sort} 1;
     val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
-      Typedef.add_typedef_global false (name, [], NoSyn) set NONE tac thy;
+      Typedef.add_typedef_global {overloaded = false} (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type (fst info);
@@ -68,7 +68,7 @@
     val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def]
     val thy = lthy
       |> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm]))
-      |> Class.prove_instantiation_instance (K (rtac class_thm 1))
+      |> Class.prove_instantiation_instance (fn ctxt => resolve_tac ctxt [class_thm] 1)
       |> Local_Theory.exit_global;
   in
     thy
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -248,16 +248,19 @@
       (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
     val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
 
-    val (alpha_info, lthy') = Inductive.add_inductive_i
+    val (alpha_info, lthy') = lthy
+      |> Inductive.add_inductive_i
        {quiet_mode = true, verbose = false, alt_name = Binding.empty,
         coind = false, no_elim = false, no_ind = false, skip_mono = false}
-         all_alpha_names [] all_alpha_intros [] lthy
+         all_alpha_names [] all_alpha_intros []
 
     val all_alpha_trms_loc = #preds alpha_info;
     val alpha_raw_induct_loc = #raw_induct alpha_info;
     val alpha_intros_loc = #intrs alpha_info;
     val alpha_cases_loc = #elims alpha_info;
-    val phi = Proof_Context.export_morphism lthy' lthy;
+    val phi =
+      Proof_Context.export_morphism lthy'
+        (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy);
     
     val all_alpha_trms = all_alpha_trms_loc
       |> map (Morphism.term phi) 
@@ -313,7 +316,7 @@
 
     fun tac ctxt =
       HEADGOAL 
-        (DETERM o (rtac induct_thm) 
+        (DETERM o (resolve_tac ctxt [induct_thm]) 
          THEN_ALL_NEW 
            (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt])))
   in
@@ -360,8 +363,8 @@
 
     fun tac ctxt =
       HEADGOAL 
-        (DETERM o (rtac alpha_induct_thm) 
-         THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
+        (DETERM o (resolve_tac ctxt [alpha_induct_thm]) 
+         THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt])
   in
     Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
     |> singleton (Proof_Context.export ctxt' ctxt)
@@ -392,7 +395,7 @@
   end
 
 fun distinct_tac ctxt cases_thms distinct_thms =
-  rtac notI THEN' eresolve_tac ctxt cases_thms 
+  resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms 
   THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms)
 
 fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info =
@@ -427,7 +430,7 @@
 
 fun alpha_eq_iff_tac ctxt dist_inj intros elims =
   SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE'
-  (rtac @{thm iffI} THEN' 
+  (resolve_tac ctxt @{thms iffI} THEN' 
     RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj),
            asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)])
 
@@ -465,14 +468,15 @@
   let
     val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv}
 
-    val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' assume_tac ctxt  
+    val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt  
 
     val bound_tac = 
-      EVERY' [ rtac exi_zero, 
+      EVERY' [ resolve_tac ctxt [exi_zero], 
                resolve_tac ctxt @{thms alpha_refl}, 
                asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]
   in
-    resolve_tac ctxt intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]
+    resolve_tac ctxt intros THEN_ALL_NEW
+      FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac]
   end
 
 fun raw_prove_refl ctxt alpha_result raw_dt_induct =
@@ -498,19 +502,20 @@
 fun prem_bound_tac pred_names alpha_eqvt ctxt = 
   let
     fun trans_prem_tac pred_names ctxt = 
-      SUBPROOF (fn {prems, context, ...} => 
+      SUBPROOF (fn {prems, context = ctxt', ...} => 
         let
-          val prems' = map (transform_prem1 context pred_names) prems
+          val prems' = map (transform_prem1 ctxt' pred_names) prems
         in
-          resolve_tac ctxt prems' 1
+          resolve_tac ctxt' prems' 1
         end) ctxt
     val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas}
   in
     EVERY' 
-      [ etac exi_neg,
+      [ eresolve_tac ctxt [exi_neg],
         resolve_tac ctxt @{thms alpha_sym_eqvt},
         asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps),
-        eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
+        eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN'
+        resolve_tac ctxt @{thms refl},
         trans_prem_tac pred_names ctxt] 
   end
 
@@ -527,7 +532,7 @@
     fun tac ctxt = 
       resolve_tac ctxt alpha_intros THEN_ALL_NEW 
       FIRST' [assume_tac ctxt,
-        rtac @{thm sym} THEN' assume_tac ctxt,
+        resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt,
         prem_bound_tac alpha_names alpha_eqvt ctxt]
   in
     alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt 
@@ -539,7 +544,7 @@
 (* applies cases rules and resolves them with the last premise *)
 fun ecases_tac cases = 
   Subgoal.FOCUS (fn {context = ctxt, prems, ...} =>
-    HEADGOAL (resolve_tac ctxt cases THEN' rtac (List.last prems)))
+    HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems]))
 
 fun aatac pred_names = 
   SUBPROOF (fn {context = ctxt, prems, ...} =>
@@ -547,13 +552,13 @@
   
 (* instantiates exI with the permutation p + q *)
 val perm_inst_tac =
-  Subgoal.FOCUS (fn {params, ...} => 
+  Subgoal.FOCUS (fn {context = ctxt, params, ...} => 
     let
       val (p, q) = apply2 snd (last2 params)
       val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q]
-      val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
+      val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
     in
-      HEADGOAL (rtac exi_inst)
+      HEADGOAL (resolve_tac ctxt [exi_inst])
     end)
 
 fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = 
@@ -563,13 +568,14 @@
     resolve_tac ctxt intros
     THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' 
       TRY o EVERY'   (* if binders are present *)
-        [ etac @{thm exE},
-          etac @{thm exE},
+        [ eresolve_tac ctxt @{thms exE},
+          eresolve_tac ctxt @{thms exE},
           perm_inst_tac ctxt, 
           resolve_tac ctxt @{thms alpha_trans_eqvt},
           assume_tac ctxt,
           aatac pred_names ctxt, 
-          eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
+          eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN'
+          resolve_tac ctxt @{thms refl},
           asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ])
   end
 
@@ -582,8 +588,9 @@
       asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) 
       THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt
   in
-    EVERY' [ rtac @{thm allI}, rtac @{thm impI}, 
-             ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ]
+    EVERY' [ resolve_tac ctxt @{thms allI},
+      resolve_tac ctxt @{thms impI}, 
+      ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ]
   end
 
 fun prep_trans_goal alpha_trm (arg1, arg2) =
@@ -633,7 +640,7 @@
       HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) 
   in    
     Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms))
-    (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' 
+    (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN' 
        RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans']))))
     |> chop (length alpha_trms)
   end
@@ -642,20 +649,20 @@
 (* proves that alpha_raw implies alpha_bn *)
 
 fun raw_prove_bn_imp_tac alpha_result ctxt = 
-  SUBPROOF (fn {prems, context, ...} => 
+  SUBPROOF (fn {prems, context = ctxt', ...} => 
     let
       val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result 
 
       val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
-      val prems'' = map (transform_prem1 context alpha_names) prems'
+      val prems'' = map (transform_prem1 ctxt' alpha_names) prems'
     in
       HEADGOAL 
         (REPEAT_ALL_NEW 
-           (FIRST' [ rtac @{thm TrueI}, 
-                     rtac @{thm conjI}, 
-                     resolve_tac ctxt prems', 
-                     resolve_tac ctxt prems'',
-                     resolve_tac ctxt alpha_intros ]))
+           (FIRST' [ resolve_tac ctxt' @{thms TrueI}, 
+                     resolve_tac ctxt' @{thms conjI}, 
+                     resolve_tac ctxt' prems', 
+                     resolve_tac ctxt' prems'',
+                     resolve_tac ctxt' alpha_intros ]))
     end) ctxt
 
 
@@ -711,7 +718,7 @@
       put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv 
       permute_prod_def prod.case prod.rec})
 
-    val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset
+    val tac = (TRY o REPEAT o eresolve_tac ctxt @{thms exE}) THEN' asm_full_simp_tac simpset
   in
     alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
   end
@@ -728,7 +735,7 @@
     asm_full_simp_tac pre_simpset
     THEN' REPEAT o (resolve_tac ctxt @{thms allI impI})
     THEN' resolve_tac ctxt alpha_intros
-    THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset)
+    THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset)
   end
 
 fun raw_constrs_rsp ctxt alpha_result constrs simps =
@@ -796,21 +803,21 @@
  by (simp add: rel_fun_def)}
 
 fun raw_prove_perm_bn_tac alpha_result simps ctxt = 
-  SUBPROOF (fn {prems, context, ...} => 
+  SUBPROOF (fn {prems, context = ctxt', ...} => 
     let
       val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result 
       val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
-      val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems'
+      val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems'
     in
       HEADGOAL 
-        (simp_tac (put_simpset HOL_basic_ss ctxt addsimps (simps @ prems'))
+        (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems'))
          THEN' TRY o REPEAT_ALL_NEW 
-           (FIRST' [ rtac @{thm TrueI}, 
-                     rtac @{thm conjI}, 
-                     rtac @{thm refl},
-                     resolve_tac ctxt prems', 
-                     resolve_tac ctxt prems'',
-                     resolve_tac ctxt alpha_intros ]))
+           (FIRST' [ resolve_tac ctxt' @{thms TrueI}, 
+                     resolve_tac ctxt' @{thms conjI}, 
+                     resolve_tac ctxt' @{thms refl},
+                     resolve_tac ctxt' prems', 
+                     resolve_tac ctxt' prems'',
+                     resolve_tac ctxt' alpha_intros ]))
     end) ctxt
 
 fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_quot.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -61,7 +61,7 @@
     val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, NONE))) qtys_descr qty_args1
     val qty_args3 = qty_args2 ~~ alpha_equivp_thms
   in
-    fold_map Quotient_Type.add_quotient_type qty_args3 lthy
+    fold_map (Quotient_Type.add_quotient_type {overloaded = false}) qty_args3 lthy
   end 
 
 (* a wrapper for lifting a raw constant *)
@@ -73,7 +73,7 @@
     val rhs_raw = rconst
 
     val raw_var = (Binding.name qconst_name, NONE, mx')
-    val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy
+    val ((binding, _, mx), ctxt) = Proof_Context.cert_var raw_var lthy
     val lhs = Syntax.check_term ctxt lhs_raw
     val rhs = Syntax.check_term ctxt rhs_raw
 
@@ -91,7 +91,9 @@
   let
     val (qconst_infos, lthy') = 
       fold_map (lift_raw_const qtys) consts_specs lthy
-    val phi = Proof_Context.export_morphism lthy' lthy
+    val phi =
+      Proof_Context.export_morphism lthy'
+        (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy)
   in
     (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy')
   end
@@ -153,14 +155,14 @@
       |> fst
 end
 
-fun unraw_vars_thm thm =
+fun unraw_vars_thm ctxt thm =
   let
     fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
 
     val vars = Term.add_vars (Thm.prop_of thm) []
-    val vars' = map (Var o unraw_var_str) vars
+    val vars' = map (Thm.cterm_of ctxt o Var o unraw_var_str) vars
   in
-    Thm.certify_instantiate ([], (vars ~~ vars')) thm
+    Thm.instantiate ([], (vars ~~ vars')) thm
   end
 
 fun unraw_bounds_thm th =
@@ -174,7 +176,7 @@
 fun lift_thms qtys simps thms ctxt =
   (map (Quotient_Tacs.lifted ctxt qtys simps
         #> unraw_bounds_thm
-        #> unraw_vars_thm
+        #> unraw_vars_thm ctxt
         #> Drule.zero_var_indexes) thms, ctxt)
 
 
@@ -228,13 +230,13 @@
       |> HOLogic.mk_Trueprop
 
     val tac = 
-      EVERY' [ rtac @{thm supports_finite},
+      EVERY' [ resolve_tac ctxt' @{thms supports_finite},
                resolve_tac ctxt' qsupports_thms,
                asm_simp_tac (put_simpset HOL_ss ctxt'
                 addsimps @{thms finite_supp supp_Pair finite_Un}) ]
   in
     Goal.prove ctxt' [] [] goals
-      (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
+      (K (HEADGOAL (resolve_tac ctxt' [qinduct] THEN_ALL_NEW tac)))
     |> singleton (Proof_Context.export ctxt' ctxt)
     |> Old_Datatype_Aux.split_conj_thm
     |> map zero_var_indexes
@@ -500,7 +502,7 @@
       @ @{thms finite.intros finite_Un finite_set finite_fset}  
   in
     Goal.prove ctxt [] [] goal
-      (K (HEADGOAL (rtac @{thm at_set_avoiding1}
+      (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding1}
           THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss)))))
   end
 
@@ -559,7 +561,7 @@
   let
     fun aux_tac prem bclauses =
       case (get_all_binders bclauses) of
-        [] => EVERY' [rtac prem, assume_tac ctxt]
+        [] => EVERY' [resolve_tac ctxt [prem], assume_tac ctxt]
       | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>  
           let
             val parms = map (Thm.term_of o snd) params
@@ -567,18 +569,18 @@
   
             val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
             val (([(_, fperm)], fprops), ctxt') = Obtain.result
-              (fn ctxt' => EVERY1 [etac exE, 
+              (fn ctxt' => EVERY1 [eresolve_tac ctxt [exE], 
                             full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), 
-                            REPEAT o (etac @{thm conjE})]) [fthm] ctxt
+                            REPEAT o (eresolve_tac ctxt @{thms conjE})]) [fthm] ctxt
   
             val abs_eq_thms = flat 
              (map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses)
 
             val ((_, eqs), ctxt'') = Obtain.result
               (fn ctxt'' => EVERY1 
-                   [ REPEAT o (etac @{thm exE}), 
-                     REPEAT o (etac @{thm conjE}),
-                     REPEAT o (dtac setify),
+                   [ REPEAT o (eresolve_tac ctxt @{thms exE}), 
+                     REPEAT o (eresolve_tac ctxt @{thms conjE}),
+                     REPEAT o (dresolve_tac ctxt [setify]),
                      full_simp_tac (put_simpset HOL_basic_ss ctxt''
                       addsimps @{thms set_append set_simps})]) abs_eq_thms ctxt'
 
@@ -592,24 +594,24 @@
             val tac1 = SOLVED' (EVERY'
               [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
                 rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}),
-                conj_tac (DETERM o resolve_tac ctxt'' fprops') ]) 
+                conj_tac ctxt'' (DETERM o resolve_tac ctxt'' fprops') ]) 
 
             (* for equalities between constructors *)
             val tac2 = SOLVED' (EVERY' 
-              [ rtac (@{thm ssubst} OF prems),
+              [ resolve_tac ctxt [@{thm ssubst} OF prems],
                 rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms),
                 rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs),
-                conj_tac (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
+                conj_tac ctxt'' (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
 
             (* proves goal "P" *)
             val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl)
-              (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
+              (K (EVERY1 [ resolve_tac ctxt'' [prem], RANGE [tac1, tac2] ]))
               |> singleton (Proof_Context.export ctxt'' ctxt)  
           in
-            rtac side_thm 1 
+            resolve_tac ctxt [side_thm] 1 
           end) ctxt
   in
-    EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
+    EVERY1 [resolve_tac ctxt [qexhaust_thm], RANGE (map2 aux_tac prems bclausess)]
   end
 
 
@@ -726,12 +728,10 @@
           val ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params
           val vs = Term.add_vars (Thm.prop_of thm) []
           val vs_tys = map (Type.legacy_freeze_type o snd) vs
-          val vs_ctrms = map (Thm.cterm_of ctxt' o Var) vs
           val assigns = map (lookup ty_parms) vs_tys          
-          
-          val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
+          val thm' = infer_instantiate ctxt' (map #1 vs ~~ assigns) thm
         in
-          rtac thm' 1
+          resolve_tac ctxt' [thm'] 1
         end) ctxt
       THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt)
  
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -261,7 +261,9 @@
  
     val {fs, simps, inducts, ...} = info; 
 
-    val morphism = Proof_Context.export_morphism lthy'' lthy
+    val morphism =
+      Proof_Context.export_morphism lthy''
+        (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy)
     val simps_exp = map (Morphism.thm morphism) (the simps)
     val inducts_exp = map (Morphism.thm morphism) (the inducts)
     
@@ -334,7 +336,9 @@
 
       val {fs, simps, ...} = info;
 
-      val morphism = Proof_Context.export_morphism lthy'' lthy
+      val morphism =
+        Proof_Context.export_morphism lthy''
+          (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy)
       val simps_exp = map (Morphism.thm morphism) (the simps)
     in
       (fs, simps_exp, lthy'')
@@ -355,13 +359,12 @@
     val goals =
       HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
         (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
-    val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_zero} :: perm_defs)
-
-    val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames 
-               THEN_ALL_NEW asm_simp_tac simpset) 1
   in
-    Goal.prove ctxt perm_indnames [] goals (K tac)
+    Goal.prove ctxt perm_indnames [] goals
+      (fn {context = ctxt', ...} =>
+        (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW
+          asm_simp_tac
+            (put_simpset HOL_basic_ss ctxt' addsimps (@{thm permute_zero} :: perm_defs))) 1)
     |> Old_Datatype_Aux.split_conj_thm
   end
 
@@ -379,14 +382,12 @@
     val goals =
       HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
         (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
-    (* FIXME proper goal context *)
-    val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thm permute_plus} :: perm_defs)
-
-    val tac = (Old_Datatype_Aux.ind_tac induct perm_indnames
-               THEN_ALL_NEW asm_simp_tac simpset) 1
   in
-    Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (K tac)
+    Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals
+      (fn {context = ctxt', ...} =>
+        (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW
+          asm_simp_tac
+            (put_simpset HOL_basic_ss ctxt' addsimps (@{thm permute_plus} :: perm_defs))) 1)
     |> Old_Datatype_Aux.split_conj_thm 
   end
 
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_eqvt.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -33,7 +33,7 @@
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro =
   let
     val cpi = Thm.cterm_of ctxt pi
-    val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
+    val pi_intro_rule = Thm.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
     val eqvt_sconfig = eqvt_strict_config addexcls pred_names
     val simps1 = 
       put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all}
@@ -47,7 +47,8 @@
         val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems'
         val prems''' = map (simplify simps2 o simplify simps1) prems''
       in
-        HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac ctxt (prems' @ prems'' @ prems'''))
+        HEADGOAL (resolve_tac ctxt [intro] THEN_ALL_NEW
+          resolve_tac ctxt (prems' @ prems'' @ prems'''))
       end) ctxt
   end
 
@@ -55,7 +56,7 @@
   let
     val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros
   in
-    EVERY' ((DETERM o rtac induct) :: cases)
+    EVERY' ((DETERM o resolve_tac ctxt [induct]) :: cases)
   end
 
 
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_function.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -151,7 +151,7 @@
       let
         val NominalFunctionResult {fs, R, psimps, simple_pinducts,
           termination, domintros, cases, eqvts, ...} =
-          cont (Thm.close_derivation proof)
+          cont lthy (Thm.close_derivation proof)
   
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
@@ -214,7 +214,7 @@
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
-    |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
+    |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
   end
 
 val nominal_function =
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_function_core.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -22,7 +22,7 @@
         * thm list (* GIntros *)
         * thm (* Ginduct *) 
         * thm  (* goalstate *)
-        * (thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
+        * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* continuation *)
        ) * local_theory
 
   val inductive_def : (binding * typ) * mixfix -> term list -> local_theory 
@@ -520,7 +520,7 @@
     val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
 
     val exactly_one =
-      ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
+      ex1I |> Thm.instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)]
       |> curry (op COMP) existence
       |> curry (op COMP) uniqueness
       |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym])
@@ -556,7 +556,7 @@
     val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
-      |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
+      |> Thm.instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)]
     val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))
     val ih_inv =  ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop}))
 
@@ -602,6 +602,7 @@
   let 
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
+      |> Config.put Inductive.inductive_internals true
       |> Proof_Context.concealed
       |> Inductive.add_inductive_i
           {quiet_mode = true,
@@ -616,6 +617,7 @@
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
           [] (* no special monos *)
       ||> Proof_Context.restore_naming lthy
+      ||> Config.put Inductive.inductive_internals (Config.get lthy Inductive.inductive_internals)
 
     val cert = Thm.cterm_of lthy
     fun requantify orig_intro thm =
@@ -849,9 +851,9 @@
       subset_induct_rule
       |> Thm.forall_intr (Thm.cterm_of ctxt D)
       |> Thm.forall_elim (Thm.cterm_of ctxt acc_R)
-      |> atac 1 |> Seq.hd
+      |> assume_tac ctxt 1 |> Seq.hd
       |> (curry op COMP) (acc_downward
-        |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)]
+        |> (Thm.instantiate' [SOME (Thm.ctyp_of ctxt domT)]
              (map (SOME o Thm.cterm_of ctxt) [R, x, z]))
         |> Thm.forall_intr (Thm.cterm_of ctxt z)
         |> Thm.forall_intr (Thm.cterm_of ctxt x))
@@ -1063,11 +1065,8 @@
       (prove_stuff lthy globals G f R xclauses complete compat
          compat_store G_elim G_eqvt invariant) f_defthm
      
-    fun mk_partial_rules provedgoal =
+    fun mk_partial_rules newctxt provedgoal =
       let
-        val newthy = Thm.theory_of_thm provedgoal (*FIXME*)
-        val newctxt = Proof_Context.init_global newthy (*FIXME*)
-
         val ((graph_is_function, complete_thm), graph_is_eqvt) =
           provedgoal
           |> Conjunction.elim
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_induct.ML
--- a/Nominal/nominal_induct.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_induct.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -5,9 +5,8 @@
 
 structure NominalInduct:
 sig
-  val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
-    (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> Rule_Cases.cases_tactic
-
+  val nominal_induct_tac: bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> context_tactic
   val nominal_induct_method: (Proof.context -> Proof.method) context_parser
 end =
 
@@ -19,7 +18,7 @@
 fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts;
 
 fun tuple_fun Ts (xi, T) =
-  Library.funpow (length Ts) HOLogic.mk_split
+  Library.funpow (length Ts) HOLogic.mk_case_prod
     (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T));
 
 fun split_all_tuples ctxt =
@@ -57,9 +56,9 @@
       end;
      val substs =
        map2 subst insts concls |> flat |> distinct (op =)
-       |> map (apply2 (Thm.cterm_of ctxt));
+       |> map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of ctxt u));
   in 
-    (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
+    (((cases, nconcls), consumes), infer_instantiate ctxt substs joined_rule) 
   end;
 
 fun rename_params_rule internal xs rule =
@@ -79,12 +78,12 @@
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn prop
       in Logic.list_implies (map rename As, C) end;
-  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
+  in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;
 
 
 (* nominal_induct_tac *)
 
-fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
+fun nominal_induct_tac simp def_insts avoiding fixings rules facts i (ctxt, st) =
   let
     val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
     val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs;
@@ -97,8 +96,8 @@
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r
       in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
-  in
-    (fn i => fn st =>
+
+    fun context_tac _ _ =
       rules
       |> inst_mutual_rule ctxt insts avoiding
       |> Rule_Cases.consume ctxt (flat defs) facts
@@ -111,7 +110,7 @@
               val xs = nth_list fixings (j - 1);
               val k = nth concls (j - 1) + more_consumes
             in
-              Method.insert_tac (more_facts @ adefs) THEN'
+              Method.insert_tac ctxt (more_facts @ adefs) THEN'
                 (if simp then
                    Induct.rotate_tac k (length adefs) THEN'
                    Induct.arbitrary_tac defs_ctxt k
@@ -124,13 +123,15 @@
             Induct.guess_instance ctxt
               (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
             |> Seq.maps (fn rule' =>
-              CASES (rule_cases ctxt rule' cases)
-                (Tactic.rtac (rename_params_rule false [] rule') i THEN
-                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
-    THEN_ALL_NEW_CASES
+              CONTEXT_CASES (rule_cases ctxt rule' cases)
+                (resolve_tac ctxt [rename_params_rule false [] rule'] i THEN
+                  PRIMITIVE
+                    (singleton (Proof_Context.export defs_ctxt
+                      (Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) ctxt)))) (ctxt, st'))));
+  in
+    (context_tac CONTEXT_THEN_ALL_NEW
       ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
-        else K all_tac)
-       THEN_ALL_NEW Induct.rulify_tac ctxt)
+        else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt)) i (ctxt, st)
   end;
 
 
@@ -173,8 +174,8 @@
   Scan.lift (Args.mode Induct.no_simpN) -- 
     (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
       avoiding -- fixing -- rule_spec) >>
-  (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
-    HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
+  (fn (no_simp, (((x, y), z), w)) => fn _ => fn facts =>
+    nominal_induct_tac (not no_simp) x y z w facts 1);
 
 end
 
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_inductive.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -24,11 +24,11 @@
 fun mk_cminus p =
   Thm.apply @{cterm "uminus :: perm => perm"} p
 
-fun minus_permute_intro_tac p =
-  rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE})
+fun minus_permute_intro_tac ctxt p =
+  resolve_tac ctxt [Thm.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}]
 
 fun minus_permute_elim p thm =
-  thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
+  thm RS (Thm.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
 
 (* fixme: move to nominal_library *)
 fun real_head_of (@{term Trueprop} $ t) = real_head_of t
@@ -156,23 +156,23 @@
 val all_elims = 
   let
     fun spec' ct =
-      Drule.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
+      Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
   in
     fold (fn ct => fn th => th RS spec' ct)
   end
 
 fun helper_tac flag prm p ctxt =
-  Subgoal.SUBPROOF (fn {context, prems, ...} =>
+  Subgoal.SUBPROOF (fn {context = ctxt', prems, ...} =>
     let
       val prems' = prems
         |> map (minus_permute_elim p)
-        |> map (eqvt_srule context)
+        |> map (eqvt_srule ctxt')
 
       val prm' = (prems' MRS prm)
         |> flag ? (all_elims [p])
-        |> flag ? (eqvt_srule context)
+        |> flag ? (eqvt_srule ctxt')
     in
-      asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
+      asm_full_simp_tac (put_simpset HOL_ss ctxt' addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
     end) ctxt
 
 fun non_binder_tac prem intr_cvars Ps ctxt = 
@@ -183,15 +183,15 @@
       val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 
       val prem' = prem
-        |> cterm_instantiate (intr_cvars ~~ p_prms) 
-        |> eqvt_srule ctxt
+        |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms) 
+        |> eqvt_srule ctxt'
 
       (* for inductive-premises*)
       fun tac1 prm = helper_tac true prm p ctxt'
 
       (* for non-inductive premises *)   
       fun tac2 prm =  
-        EVERY' [ minus_permute_intro_tac p, 
+        EVERY' [ minus_permute_intro_tac ctxt' p, 
                  eqvt_stac ctxt', 
                  helper_tac false prm p ctxt' ]
 
@@ -199,7 +199,7 @@
         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
     in
       EVERY1 [ eqvt_stac ctxt', 
-               rtac prem', 
+               resolve_tac ctxt' [prem'], 
                RANGE (map (SUBGOAL o select) prems) ]
     end) ctxt
 
@@ -217,8 +217,9 @@
     val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss)
   in 
     Goal.prove ctxt [] [] fresh_goal
-      (K (HEADGOAL (rtac @{thm at_set_avoiding2} 
-          THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp])))
+      (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2}
+          THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o
+            eresolve_tac ctxt @{thms conjE}, simp])))
   end
 
 val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x" 
@@ -238,27 +239,27 @@
       val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm 
       val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args 
       
-      val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm
+      val user_thm' = map (infer_instantiate ctxt (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ prms)) user_thm
         |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems)))
       
       val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm'
 
       val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result
-              (K (EVERY1 [etac @{thm exE}, 
+              (K (EVERY1 [eresolve_tac ctxt @{thms exE}, 
                           full_simp_tac (put_simpset HOL_basic_ss ctxt
                             addsimps @{thms supp_Pair fresh_star_Un}),
-                          REPEAT o etac @{thm conjE},
-                          dtac fresh_star_plus,
-                          REPEAT o dtac supp_perm_eq'])) [fthm] ctxt 
+                          REPEAT o eresolve_tac ctxt @{thms conjE},
+                          dresolve_tac ctxt [fresh_star_plus],
+                          REPEAT o dresolve_tac ctxt [supp_perm_eq']])) [fthm] ctxt 
 
       val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs)
       fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt
 
-      val cperms = map (Thm.cterm_of ctxt o perm_const) prm_tys
+      val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
       val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms 
       val prem' = prem
-        |> cterm_instantiate (intr_cvars ~~ qp_prms)
-        |> eqvt_srule ctxt
+        |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms)
+        |> eqvt_srule ctxt'
 
       val fprop' = eqvt_srule ctxt' fprop 
       val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop'])
@@ -268,8 +269,8 @@
 
       (* for non-inductive premises *)   
       fun tac2 prm =  
-        EVERY' [ minus_permute_intro_tac (mk_cplus q p), 
-                 eqvt_stac ctxt, 
+        EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p), 
+                 eqvt_stac ctxt', 
                  helper_tac false prm (mk_cplus q p) ctxt' ]
 
       fun select prm (t, i) =
@@ -279,11 +280,11 @@
         (fn {context = ctxt'', ...} => 
            EVERY1 [ CONVERSION (expand_conv_bot ctxt''),
                     eqvt_stac ctxt'',
-                    rtac prem',
+                    resolve_tac ctxt'' [prem'],
                     RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
         |> singleton (Proof_Context.export ctxt' ctxt)
     in
-      rtac side_thm 1
+      resolve_tac ctxt [side_thm] 1
     end) ctxt
 
 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args =
@@ -291,17 +292,17 @@
     val tac1 = non_binder_tac prem intr_cvars Ps ctxt
     val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt
   in 
-    EVERY' [ rtac @{thm allI}, rtac @{thm allI}, 
+    EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms allI}, 
              if null avoid then tac1 else tac2 ]
   end
 
 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args 
-  {prems, context} =
+  {prems, context = ctxt} =
   let
     val cases_tac = 
-      map7 (case_tac context Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args
+      map7 (case_tac ctxt Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args
   in 
-    EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ]
+    EVERY1 [ DETERM o resolve_tac ctxt [raw_induct], RANGE cases_tac ]
   end
 
 val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp}
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_library.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -104,7 +104,7 @@
   val atomize_concl: Proof.context -> thm -> thm
 
   (* applies a tactic to a formula composed of conjunctions *)
-  val conj_tac: (int -> tactic) -> int -> tactic
+  val conj_tac: Proof.context -> (int -> tactic) -> int -> tactic
 end
 
 
@@ -450,9 +450,9 @@
     val monos = Inductive.get_monos ctxt
     val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def}
   in
-    EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 
+    EVERY [cut_facts_tac [thm] 1, eresolve_tac ctxt [rev_mp] 1, 
       REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)),
-      REPEAT_DETERM (rtac impI 1 THEN (assume_tac ctxt 1 ORELSE tac))]
+      REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))]
   end
 
 fun map_thm ctxt f tac thm =
@@ -485,10 +485,10 @@
 | split_conj2 _ _ = NONE;
 
 fun transform_prem1 ctxt names thm =
-  map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm
+  map_thm ctxt (split_conj1 names) (eresolve_tac ctxt [conjunct1] 1) thm
 
 fun transform_prem2 ctxt names thm =
-  map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm
+  map_thm ctxt (split_conj2 names) (eresolve_tac ctxt [conjunct2] 1) thm
 
 
 (* transforms a theorem into one of the object logic *)
@@ -499,12 +499,13 @@
 
 
 (* applies a tactic to a formula composed of conjunctions *)
-fun conj_tac tac i =
+fun conj_tac ctxt tac i =
   let
      fun select (trm, i) =
        case trm of
          @{term "Trueprop"} $ t' => select (t', i)
-       | @{term "op &"} $ _ $ _ => EVERY' [rtac @{thm conjI}, RANGE [conj_tac tac, conj_tac tac]] i
+       | @{term "op &"} $ _ $ _ =>
+          EVERY' [resolve_tac ctxt @{thms conjI}, RANGE [conj_tac ctxt tac, conj_tac ctxt tac]] i
        | _ => tac i
   in
     SUBGOAL select i
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_mutual.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -19,7 +19,7 @@
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
-        * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
+        * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
        ) * local_theory)
 end
 
@@ -330,21 +330,23 @@
 
     val induct_thm = case induct_thms of
         [thm] => thm
-          |> Drule.gen_all (Variable.maxidx_of ctxt')
+          |> Variable.gen_all ctxt'
           |> Thm.permute_prems 0 1
           |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm)
       | thms => thms
-          |> map (Drule.gen_all (Variable.maxidx_of ctxt'))
+          |> map (Variable.gen_all ctxt')
           |> map (Rule_Cases.add_consumes 1)
           |> snd o Rule_Cases.strict_mutual_rule ctxt'
           |> atomize_concl ctxt'
 
     fun tac ctxt thm =
-      rtac (Drule.gen_all (Variable.maxidx_of ctxt) thm) THEN_ALL_NEW assume_tac ctxt
+      resolve_tac ctxt [Variable.gen_all ctxt thm]
+        THEN_ALL_NEW assume_tac ctxt
   in
     Goal.prove ctxt' (flat arg_namess) [] goal
       (fn {context = ctxt'', ...} =>
-        HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map (tac ctxt'') eqvts_thms)))
+        HEADGOAL (DETERM o (resolve_tac ctxt'' [induct_thm]) THEN'
+          RANGE (map (tac ctxt'') eqvts_thms)))
     |> singleton (Proof_Context.export ctxt' ctxt)
     |> split_conj_thm
     |> map (fn th => th RS mp)
@@ -441,7 +443,7 @@
     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'
+    fun mutual_cont ctxt = mk_partial_rules_mutual lthy''' (cont ctxt) mutual'
 
     (* proof of equivalence between graph and auxiliary graph *)
     val x = Var(("x", 0), ST)
@@ -474,22 +476,25 @@
     val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms
 
     val inj_thm = Goal.prove lthy''' [] [] goal_inj 
-      (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1)))
+      (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct]
+        THEN_ALL_NEW asm_simp_tac simpset1)))
 
     fun aux_tac thm = 
-      rtac (Drule.gen_all (Variable.maxidx_of lthy''') thm) THEN_ALL_NEW
+      resolve_tac lthy''' [Variable.gen_all lthy''' thm] THEN_ALL_NEW
       asm_full_simp_tac (simpset1 addsimps [inj_thm])
     
     val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 
-      (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms))))
-      |> Drule.gen_all (Variable.maxidx_of lthy''')
+      (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct]
+        THEN' RANGE (map aux_tac GIntro_thms))))
+      |> Variable.gen_all lthy'''
     val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 
-      (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE
+      (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_induct] THEN' RANGE
         (map (aux_tac o simplify simpset0) GIntro_aux_thms))))
-      |> Drule.gen_all (Variable.maxidx_of lthy''')
+      |> Variable.gen_all lthy'''
 
     val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux)))
-      (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm]))))
+      (K (HEADGOAL (EVERY' ((map (resolve_tac lthy''' o single) @{thms ext ext iffI}) @
+        [eresolve_tac lthy''' [iff2_thm], eresolve_tac lthy''' [iff1_thm]]))))
  
     val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm]))
     val goalstate' = 
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_permeq.ML
--- a/Nominal/nominal_permeq.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_permeq.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -141,7 +141,7 @@
         val ty_insts = map SOME [b, a]
         val term_insts = map SOME [p, f, x]                        
       in
-        Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
+        Thm.instantiate' ty_insts term_insts @{thm eqvt_apply}
       end
   | _ => Conv.no_conv ctrm
 
diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_thmdecls.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -183,8 +183,9 @@
   in
     REPEAT o FIRST'
       [CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms),
-       rtac (thm RS @{thm "trans"}),
-       rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}]
+       resolve_tac ctxt [thm RS @{thm trans}],
+       resolve_tac ctxt @{thms trans[OF "permute_fun_def"]} THEN'
+       resolve_tac ctxt @{thms ext}]
   end
 
 in
@@ -213,8 +214,12 @@
   let
     val ss_thms = @{thms "permute_minus_cancel"(2)}
   in
-    EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt,
-      rtac @{thm "permute_boolI"}, dtac thm', 
+    EVERY' [resolve_tac ctxt @{thms iffI},
+      dresolve_tac ctxt @{thms permute_boolE},
+      resolve_tac ctxt [thm],
+      assume_tac ctxt,
+      resolve_tac ctxt @{thms permute_boolI},
+      dresolve_tac ctxt [thm'],
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)]
   end
 
@@ -232,7 +237,7 @@
     val p = concl |> dest_comb |> snd |> find_perm
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl))
     val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
-    val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm
+    val thm' = infer_instantiate ctxt' [(#1 (dest_Var p), Thm.cterm_of ctxt' (mk_minus p'))] thm
   in
     Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1)
       |> singleton (Proof_Context.export ctxt' ctxt)