diff --git a/src/HOL/Eisbach/Tests.thy b/src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy
+++ b/src/HOL/Eisbach/Tests.thy
@@ -1,607 +1,607 @@
 (*  Title:      HOL/Eisbach/Tests.thy
     Author:     Daniel Matichuk, NICTA/UNSW
 *)
 
 section \<open>Miscellaneous Eisbach tests\<close>
 
 theory Tests
 imports Main Eisbach_Tools
 begin
 
 
 subsection \<open>Named Theorems Tests\<close>
 
 named_theorems foo
 
 method foo declares foo = (rule foo)
 
 lemma
   assumes A [foo]: A
   shows A
   apply foo
   done
 
 method abs_used for P = (match (P) in "\<lambda>a. ?Q" \<Rightarrow> fail \<bar> _ \<Rightarrow> -)
 
 
 subsection \<open>Match Tests\<close>
 
 notepad
 begin
   have dup: "\<And>A. A \<Longrightarrow> A \<Longrightarrow> A" by simp
 
   fix A y
   have "(\<And>x. A x) \<Longrightarrow> A y"
     apply (rule dup, match premises in Y: "\<And>B. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
     apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
     apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P y" for y \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=y]\<close>\<close>)
     apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P z" for z \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=z]\<close>\<close>)
     apply (rule dup, match conclusion in "P y" for P \<Rightarrow> \<open>match premises in Y: "\<And>z. P z" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
     apply (match premises in Y: "\<And>z :: 'a. P z" for P \<Rightarrow> \<open>match conclusion in "P y" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
     done
 
   assume X: "\<And>x. A x" "A y"
   have "A y"
     apply (match X in Y:"\<And>B. A B" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>)
     apply (match X in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
     apply (match X in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B, print_term x\<close>)
     apply (insert X)
     apply (match premises in Y:"\<And>B. A B" and Y':"B y" for B and y :: 'a \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>)
     apply (match premises in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
     apply (match premises in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
     apply (match conclusion in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
     apply assumption
     done
 
   {
    fix B x y
    assume X: "\<And>x y. B x x y"
    have "B x x y"
      by (match X in Y:"\<And>y. B y y z" for z \<Rightarrow> \<open>rule Y[where y=x]\<close>)
 
    fix A B
    have "(\<And>x y. A (B x) y) \<Longrightarrow> A (B x) y"
      by (match premises in Y: "\<And>xx. ?H (B xx)" \<Rightarrow> \<open>rule Y\<close>)
   }
 
   (* match focusing retains prems *)
   fix B x
   have "(\<And>x. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x"
     apply (match premises in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match premises in Y': "\<And>z :: 'b. B z" \<Rightarrow> \<open>print_fact Y, print_fact Y', rule Y'[where z=x]\<close>\<close>)
     done
 
   (*Attributes *)
   fix C
   have "(\<And>x :: 'a. A x)  \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x \<and> B x \<and> A y"
     apply (intro conjI)
     apply (match premises in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce)
     apply (match premises in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce\<close>)
     apply (match premises in Y[thin]: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>print_fact Y,fail\<close> \<bar> _ \<Rightarrow> \<open>print_fact Y\<close>)\<close>)
     (*apply (match premises in Y: "\<And>z :: 'b. B z"  \<Rightarrow> \<open>(match premises in Y'[thin]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> fail \<bar> Y': _ \<Rightarrow> -)\<close>)\<close>)*)
     apply assumption
     done
 
   fix A B C D
   have "\<And>uu'' uu''' uu uu'. (\<And>x :: 'a. A uu' x)  \<Longrightarrow> D uu y \<Longrightarrow> (\<And>z. B uu z) \<Longrightarrow> C uu y \<Longrightarrow> (\<And>z y. C uu z)  \<Longrightarrow> B uu x \<and> B uu x \<and> C uu y"
     apply (match premises in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
                           Y'[thin]: "\<And>rr :: 'b. B ?zz rr" \<Rightarrow>
           \<open>print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]\<close>)
     apply (match premises in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
     apply (insert TrueI)
     apply (match premises in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
     apply assumption
     done
 
 
   (* Multi-matches. As many facts as match are bound. *)
   fix A B C x
   have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
     apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
     apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *)
     apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
     done
 
   fix A B C x
   have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
     apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
     apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *)
     apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
     done
 
   fix A B C P Q and x :: 'a and y :: 'a
   have "(\<And>x y :: 'a. A x y \<and> Q) \<Longrightarrow> (\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q) \<Longrightarrow> (\<And>x y. C (x :: 'a) (y :: 'a) \<and> P) \<Longrightarrow> A y x \<and> B y x"
     by (match premises in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule conjI, rule Y[where z=x,THEN conjunct1], rule Y[THEN conjunct1]\<close>)
 
 
   (*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *)
   fix A B C x
   have "(\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> (\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
     apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow>
                                   \<open>match (P) in B \<Rightarrow> fail
                                         \<bar> "\<lambda>a. B" \<Rightarrow> fail
                                         \<bar> _ \<Rightarrow> -,
                                   intro conjI, (rule Y[THEN conjunct1])\<close>)
     apply (rule dup)
     apply (match premises in Y':"\<And>x :: 'a. ?U x \<and> Q x" and Y: "\<And>x :: 'a. Q x \<and> ?U x" (multi)  for Q \<Rightarrow> \<open>insert Y[THEN conjunct1]\<close>)
     apply assumption (* Previous match requires that Q is consistent *)
     apply (match premises in Y: "\<And>z :: 'a. ?A z \<longrightarrow> False" (multi) \<Rightarrow> \<open>print_fact Y, fail\<close> \<bar> "C y" \<Rightarrow> \<open>print_term C\<close>) (* multi-match must bind something *)
     apply (match premises in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
     apply (match premises in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
     done
 
   (* All bindings must be tried for a particular theorem.
      However all combinations are NOT explored. *)
   fix B A C
   assume asms:"\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q" "\<And>x :: 'a. A x x \<and> Q" "\<And>a b. C (a :: 'a) (b :: 'a) \<and> Q"
   have "B y x \<and> C x y \<and> B x y \<and> C y x \<and> A x x"
     apply (intro conjI)
     apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>)
     apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>)
     apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>)
     apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>)
     apply (match asms in Y: "\<And>z a. A (z :: 'a) (a :: 'a) \<and> R"  for R \<Rightarrow> fail \<bar> _ \<Rightarrow> -)
     apply (rule asms[THEN conjunct1])
     done
 
   (* Attributes *)
   fix A B C x
   have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
     apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct1]  in Y':"?H"  (multi) \<Rightarrow> \<open>intro conjI,rule Y'\<close>\<close>)
     apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct2]  in Y':"?H"  (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
     apply assumption
     done
 
 (* Removed feature for now *)
 (*
   fix A B C x
   have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
   apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match \<open>K @{thms Y TrueI}\<close> in Y':"?H"  (multi) \<Rightarrow> \<open>rule conjI; (rule Y')?\<close>\<close>)
   apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match \<open>K [@{thm Y}]\<close> in Y':"?H"  (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
   done
 *)
   (* Testing THEN_ALL_NEW within match *)
   fix A B C x
   have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
     apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI ; ((rule Y[THEN conjunct1])?); rule Y[THEN conjunct2] \<close>)
     done
 
   (* Cut tests *)
   fix A B C D
 
   have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
     by (((match premises in I: "P \<and> Q" (cut)
               and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?), simp)
 
   have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
     by (match premises in I: "P \<and> Q" (cut 2)
               and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)
 
   have "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
     by (((match premises in I: "P \<and> Q" (cut)
               and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?, simp) | simp)
 
   fix f x y
   have "f x y \<Longrightarrow> f x y"
     by (match conclusion in "f x y" for f x y  \<Rightarrow> \<open>print_term f\<close>)
 
   fix A B C
   assume X: "A \<and> B" "A \<and> C" C
   have "A \<and> B \<and> C"
     by (match X in H: "A \<and> ?H" (multi, cut) \<Rightarrow>
           \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> fail\<close>
         | simp add: X)
 
 
   (* Thinning an inner focus *)
   (* Thinning should persist within a match, even when on an external premise *)
 
   fix A
   have "(\<And>x. A x \<and> B) \<Longrightarrow> B \<and> C \<Longrightarrow> C"
     apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow>
                      \<open>match premises in H'[thin]: "\<And>x. A x \<and> B" \<Rightarrow>
                       \<open>match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail
                                          \<bar> _ \<Rightarrow> -\<close>
                       ,match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail \<bar> _ \<Rightarrow> -\<close>)
     apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow> fail
                               \<bar> H':_ \<Rightarrow> \<open>rule H'[THEN conjunct2]\<close>)
     done
 
 
   (* Local premises *)
   (* Only match premises which actually existed in the goal we just focused.*)
 
   fix A
   assume asms: "C \<and> D"
   have "B \<and> C \<Longrightarrow> C"
     by (match premises in _ \<Rightarrow> \<open>insert asms,
             match premises (local) in "B \<and> C" \<Rightarrow> fail
                                   \<bar> H:"C \<and> D" \<Rightarrow> \<open>rule H[THEN conjunct1]\<close>\<close>)
 end
 
 
 
 (* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
    by retrofitting. This needs to be done more carefully to avoid smashing
    legitimate pairs.*)
 
 schematic_goal "?A x \<Longrightarrow> A x"
   apply (match conclusion in "H" for H \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
   apply assumption
   done
 
 (* Ensure short-circuit after first match failure *)
 lemma
   assumes A: "P \<and> Q"
   shows "P"
   by ((match A in "P \<and> Q" \<Rightarrow> fail \<bar> "?H" \<Rightarrow> -) | simp add: A)
 
 lemma
   assumes A: "D \<and> C" "A \<and> B" "A \<longrightarrow> B"
   shows "A"
   apply ((match A in U: "P \<and> Q" (cut) and "P' \<longrightarrow> Q'" for P Q P' Q' \<Rightarrow>
       \<open>simp add: U\<close> \<bar> "?H" \<Rightarrow> -) | -)
   apply (simp add: A)
   done
 
 
 subsection \<open>Uses Tests\<close>
 
 ML \<open>
   fun test_internal_fact ctxt factnm =
-    (case try (Proof_Context.get_thms ctxt) factnm of
+    (case \<^try>\<open>Proof_Context.get_thms ctxt factnm\<close> of
       NONE => ()
     | SOME _ => error "Found internal fact");
 \<close>
 
 method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses)
 
 lemma assumes A shows A by (uses_test\<^sub>1 uses_test\<^sub>1_uses: assms)
 
 ML \<open>test_internal_fact \<^context> "uses_test\<^sub>1_uses"\<close>
 
 ML \<open>test_internal_fact \<^context> "Tests.uses_test\<^sub>1_uses"\<close>
 ML \<open>test_internal_fact \<^context> "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close>
 
 subsection \<open>Basic fact passing\<close>
 
 method find_fact for x y :: bool uses facts1 facts2 =
   (match facts1 in U: "x" \<Rightarrow> \<open>insert U,
       match facts2 in U: "y" \<Rightarrow> \<open>insert U\<close>\<close>)
 
 lemma assumes A: A and B: B shows "A \<and> B"
   apply (find_fact "A" "B" facts1: A facts2: B)
   apply (rule conjI; assumption)
   done
 
 
 subsection \<open>Testing term and fact passing in recursion\<close>
 
 
 method recursion_example for x :: bool uses facts =
   (match (x) in
     "A \<and> B" for A B \<Rightarrow> \<open>(recursion_example A facts: facts, recursion_example B facts: facts)\<close>
   \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>)
 
 lemma
   assumes asms: "A" "B" "C" "D"
   shows "(A \<and> B) \<and> (C \<and> D)"
   apply (recursion_example "(A \<and> B) \<and> (C \<and> D)" facts: asms)
   apply simp
   done
 
 (* uses facts are not accumulated *)
 
 method recursion_example' for A :: bool and B :: bool uses facts =
   (match facts in
     H: "A" and H': "B" \<Rightarrow> \<open>recursion_example' "A" "B" facts: H TrueI\<close>
   \<bar> "A" and "True" \<Rightarrow> \<open>recursion_example' "A" "B" facts: TrueI\<close>
   \<bar> "True" \<Rightarrow> -
   \<bar> "PROP ?P" \<Rightarrow> fail)
 
 lemma
   assumes asms: "A" "B"
   shows "True"
   apply (recursion_example' "A" "B" facts: asms)
   apply simp
   done
 
 
 (*Method.sections in existing method*)
 method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = (simp add: my_simp\<^sub>1_facts)
 lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms)
 
 (*Method.sections via Eisbach argument parser*)
 method uses_test\<^sub>2 uses uses_test\<^sub>2_uses = (uses_test\<^sub>1 uses_test\<^sub>1_uses: uses_test\<^sub>2_uses)
 lemma assumes A shows A by (uses_test\<^sub>2 uses_test\<^sub>2_uses: assms)
 
 
 subsection \<open>Declaration Tests\<close>
 
 named_theorems declare_facts\<^sub>1
 
 method declares_test\<^sub>1 declares declare_facts\<^sub>1 = (rule declare_facts\<^sub>1)
 
 lemma assumes A shows A by (declares_test\<^sub>1 declare_facts\<^sub>1: assms)
 
 lemma assumes A[declare_facts\<^sub>1]: A shows A by declares_test\<^sub>1
 
 
 subsection \<open>Rule Instantiation Tests\<close>
 
 method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   (erule allE [where x = x and P = P])
 
 lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>1 x Q)
 
 method my_allE\<^sub>2 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   (erule allE [of P x])
 
 lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>2 x Q)
 
 method my_allE\<^sub>3 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
     \<open>erule X [where x = x and P = P]\<close>)
 
 lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>3 x Q)
 
 method my_allE\<^sub>4 for x :: 'a and P :: "'a \<Rightarrow> bool" =
   (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
     \<open>erule X [of x P]\<close>)
 
 lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>4 x Q)
 
 
 
 subsection \<open>Polymorphism test\<close>
 
 axiomatization foo' :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool"
 axiomatization where foo'_ax1: "foo' x y z \<Longrightarrow> z \<and> y"
 axiomatization where foo'_ax2: "foo' x y y \<Longrightarrow> x \<and> z"
 axiomatization where foo'_ax3: "foo' (x :: int) y y \<Longrightarrow> y \<and> y"
 
 lemmas my_thms = foo'_ax1 foo'_ax2 foo'_ax3
 
 definition first_id where "first_id x = x"
 
 lemmas my_thms' = my_thms[of "first_id x" for x]
 
 method print_conclusion = (match conclusion in concl for concl \<Rightarrow> \<open>print_term concl\<close>)
 
 lemma
   assumes foo: "\<And>x (y :: bool). foo' (A x) B (A x)"
   shows "\<And>z. A z \<and> B"
   apply
     (match conclusion in "f x y" for f y and x :: "'d :: type" \<Rightarrow> \<open>
       match my_thms' in R:"\<And>(x :: 'f :: type). ?P (first_id x) \<Longrightarrow> ?R"
                      and R':"\<And>(x :: 'f :: type). ?P' (first_id x) \<Longrightarrow> ?R'" \<Rightarrow> \<open>
         match (x) in "q :: 'f" for q \<Rightarrow> \<open>
           rule R[of q,simplified first_id_def],
           print_conclusion,
           rule foo
       \<close>\<close>\<close>)
   done
 
 
 subsection \<open>Unchecked rule instantiation, with the possibility of runtime errors\<close>
 
 named_theorems my_thms_named
 
 declare foo'_ax3[my_thms_named]
 
 method foo_method3 declares my_thms_named =
   (match my_thms_named[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
 
 notepad
 begin
 
   (*FIXME: Shouldn't need unchecked keyword here. See Tests_Failing.thy *)
   fix A B x
   have "foo' x B A \<Longrightarrow> A \<and> B"
     by (match my_thms[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
 
   fix A B x
   note foo'_ax1[my_thms_named]
   have "foo' x B A \<Longrightarrow> A \<and> B"
     by (match my_thms_named[where x=z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
 
   fix A B x
   note foo'_ax1[my_thms_named] foo'_ax2[my_thms_named] foo'_ax3[my_thms_named]
   have "foo' x B A \<Longrightarrow> A \<and> B"
    by foo_method3
 
 end
 
 
 ML \<open>
 structure Data = Generic_Data
 (
   type T = thm list;
   val empty: T = [];
   val extend = I;
   fun merge data : T = Thm.merge_thms data;
 );
 \<close>
 
 local_setup \<open>Local_Theory.add_thms_dynamic (\<^binding>\<open>test_dyn\<close>, Data.get)\<close>
 
 setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close>
 
 method dynamic_thms_test = (rule test_dyn)
 
 locale foo =
   fixes A
   assumes A : "A"
 begin
 
 local_setup
   \<open>Local_Theory.declaration {pervasive = false, syntax = false}
     (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close>
 
 lemma A by dynamic_thms_test
 
 end
 
 
 notepad
 begin
   fix A x
   assume X: "\<And>x. A x"
   have "A x"
     by (match X in H[of x]:"\<And>x. A x" \<Rightarrow> \<open>print_fact H,match H in "A x" \<Rightarrow> \<open>rule H\<close>\<close>)
 
   fix A x B
   assume X: "\<And>x :: bool. A x \<Longrightarrow> B" "\<And>x. A x"
   assume Y: "A B"
   have "B \<and> B \<and> B \<and> B \<and> B \<and> B"
     apply (intro conjI)
     apply (match X in H[OF X(2)]:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H,rule H\<close>)
     apply (match X in H':"\<And>x. A x" and H[OF H']:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H',print_fact H,rule H\<close>)
     apply (match X in H[of Q]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H, rule Y\<close>)
     apply (match X in H[of Q,OF Y]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H\<close>)
     apply (match X in H[OF Y,intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>print_fact H,fastforce\<close>)
     apply (match X in H[intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>rule H[where x=B], rule Y\<close>)
     done
 
   fix x :: "prop" and A
   assume X: "TERM x"
   assume Y: "\<And>x :: prop. A x"
   have "A TERM x"
     apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
     done
 end
 
 subsection \<open>Proper context for method parameters\<close>
 
 method add_simp methods m uses f = (match f in H[simp]:_ \<Rightarrow> m)
 
 method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \<Rightarrow> m)
 
 method rule_my_thms = (rule my_thms_named)
 method rule_my_thms' declares my_thms_named = (rule my_thms_named)
 
 lemma
   assumes A: A and B: B
   shows
   "(A \<or> B) \<and> A \<and> A \<and> A"
   apply (intro conjI)
   apply (add_simp \<open>add_simp simp f: B\<close> f: A)
   apply (add_my_thms rule_my_thms f:A)
   apply (add_my_thms rule_my_thms' f:A)
   apply (add_my_thms \<open>rule my_thms_named\<close> f:A)
   done
 
 
 subsection \<open>Shallow parser tests\<close>
 
 method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail
 
 lemma True
   by (all_args True False - fail f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
 
 
 subsection \<open>Method name internalization test\<close>
 
 
 method test2 = (simp)
 
 method simp = fail
 
 lemma "A \<Longrightarrow> A" by test2
 
 
 subsection \<open>Dynamic facts\<close>
 
 named_theorems my_thms_named'
 
 method foo_method1 for x =
   (match my_thms_named' [of (unchecked) x] in R: "PROP ?H" \<Rightarrow> \<open>rule R\<close>)
 
 lemma
   assumes A [my_thms_named']: "\<And>x. A x"
   shows "A y"
   by (foo_method1 y)
 
 
 subsection \<open>Eisbach method invocation from ML\<close>
 
 method test_method for x y uses r = (print_term x, print_term y, rule r)
 
 method_setup test_method' = \<open>
   Args.term -- Args.term --
   (Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
     (fn ((x, y), r) => fn ctxt =>
       Method_Closure.apply_method ctxt \<^method>\<open>test_method\<close> [x, y] [r] [] ctxt)
 \<close>
 
 lemma
   fixes a b :: nat
   assumes "a = b"
   shows "b = a"
   apply (test_method a b)?
   apply (test_method' a b rule: refl)?
   apply (test_method' a b rule: assms [symmetric])?
   done
 
 subsection \<open>Eisbach methods in locales\<close>
 
 locale my_locale1 = fixes A assumes A: A begin
 
 method apply_A =
   (match conclusion in "A" \<Rightarrow>
     \<open>match A in U:"A" \<Rightarrow>
       \<open>print_term A, print_fact A, rule U\<close>\<close>)
 
 end
 
 locale my_locale2 = fixes B assumes B: B begin
 
 interpretation my_locale1 B by (unfold_locales; rule B)
 
 lemma B by apply_A
 
 end
 
 context fixes C assumes C: C begin
 
 interpretation my_locale1 C by (unfold_locales; rule C)
 
 lemma C by apply_A
 
 end
 
 context begin
 
 interpretation my_locale1 "True \<longrightarrow> True" by (unfold_locales; blast)
 
 lemma "True \<longrightarrow> True" by apply_A
 
 end
 
 locale locale_poly = fixes P assumes P: "\<And>x :: 'a. P x" begin
 
 method solve_P for z :: 'a = (rule P[where x = z]) 
 
 end
 
 context begin
 
 interpretation locale_poly "\<lambda>x:: nat. 0 \<le> x" by (unfold_locales; blast)
 
 lemma "0 \<le> (n :: nat)" by (solve_P n)
 
 end
 
 subsection \<open>Mutual recursion via higher-order methods\<close>
 
 experiment begin
 
 method inner_method methods passed_method = (rule conjI; passed_method)
 
 method outer_method = (inner_method \<open>outer_method\<close> | assumption)
 
 lemma "Q \<Longrightarrow> R \<Longrightarrow> P \<Longrightarrow> (Q \<and> R) \<and> P"
   by outer_method
 
 end
 
 end
diff --git a/src/HOL/Eisbach/eisbach_rule_insts.ML b/src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML
@@ -1,233 +1,233 @@
 (*  Title:      HOL/Eisbach/eisbach_rule_insts.ML
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Eisbach-aware variants of the "where" and "of" attributes.
 
 Alternate syntax for rule_insts.ML participates in token closures by
 examining the behaviour of Rule_Insts.where_rule and instantiating token
 values accordingly. Instantiations in re-interpretation are done with
 infer_instantiate.
 *)
 
 structure Eisbach_Rule_Insts: sig end =
 struct
 
 fun restore_tags thm = Thm.map_tags (K (Thm.get_tags thm));
 
 val mk_term_type_internal = Logic.protect o Logic.mk_term o Logic.mk_type;
 
 fun term_type_cases f g t = 
-  (case (try (Logic.dest_type o Logic.dest_term o Logic.unprotect) t) of
+  (case \<^try>\<open>Logic.dest_type (Logic.dest_term (Logic.unprotect t))\<close> of
     SOME T => f T
-  | NONE => 
-    (case (try Logic.dest_term t) of
-      SOME t => g t
-    | NONE => raise Fail "Lost encoded instantiation"))
+  | NONE =>
+      (case \<^try>\<open>Logic.dest_term t\<close> of
+        SOME t => g t
+      | NONE => raise Fail "Lost encoded instantiation"))
 
 fun add_thm_insts ctxt thm =
   let
     val tyvars = Thm.fold_terms Term.add_tvars thm [];
     val tyvars' = tyvars |> map (mk_term_type_internal o TVar);
 
     val tvars = Thm.fold_terms Term.add_vars thm [];
     val tvars' = tvars  |> map (Logic.mk_term o Var);
 
     val conj =
       Logic.mk_conjunction_list (tyvars' @ tvars') |> Thm.cterm_of ctxt |> Drule.mk_term;
   in
     ((tyvars, tvars), Conjunction.intr thm conj)
   end;
 
 fun get_thm_insts thm =
   let
     val (thm', insts) = Conjunction.elim thm;
 
     val insts' = insts
       |> Drule.dest_term
       |> Thm.term_of
       |> Logic.dest_conjunction_list
       |> (fn f => fold (fn t => fn (tys, ts) =>
           term_type_cases (fn T => (T :: tys, ts)) (fn t => (tys, t :: ts)) t) f ([], []))
       ||> rev
       |>> rev;
   in
     (thm', insts')
   end;
 
 fun instantiate_xis ctxt insts thm =
   let
     val tyvars = Thm.fold_terms Term.add_tvars thm [];
     val tvars = Thm.fold_terms Term.add_vars thm [];
 
     fun add_inst (xi, t) (Ts, ts) =
       (case AList.lookup (op =) tyvars xi of
         SOME S => (((xi, S), Thm.ctyp_of ctxt (Logic.dest_type t)) :: Ts, ts)
       | NONE =>
           (case AList.lookup (op =) tvars xi of
             SOME _ => (Ts, (xi, Thm.cterm_of ctxt t) :: ts)
           | NONE => error "indexname not found in thm"));
 
     val (instT, inst) = fold add_inst insts ([], []);
   in
     (Thm.instantiate (instT, []) thm
     |> infer_instantiate ctxt inst
     COMP_INCR asm_rl)
     |> Thm.adjust_maxidx_thm ~1
     |> restore_tags thm
   end;
 
 
 datatype rule_inst =
   Named_Insts of ((indexname * string) * (term -> unit)) list * (binding * string option * mixfix) list
 | Term_Insts of (indexname * term) list
 | Unchecked_Term_Insts of term option list * term option list;
 
 fun mk_pair (t, t') = Logic.mk_conjunction (Logic.mk_term t, Logic.mk_term t');
 
 fun dest_pair t = apply2 Logic.dest_term (Logic.dest_conjunction t);
 
 fun embed_indexname ((xi, s), f) =
   let fun wrap_xi xi t = mk_pair (Var (xi, fastype_of t), t);
   in ((xi, s), f o wrap_xi xi) end;
 
 fun unembed_indexname t = dest_pair t |> apfst (Term.dest_Var #> fst);
 
 fun read_where_insts (insts, fixes) =
   let
     val insts' =
       if forall (fn (_, v) => Parse_Tools.is_real_val v) insts
       then Term_Insts (map (unembed_indexname o Parse_Tools.the_real_val o snd) insts)
       else
         Named_Insts (map (fn (xi, p) => embed_indexname
           ((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts, fixes);
   in insts' end;
 
 fun of_rule thm  (args, concl_args) =
   let
     fun zip_vars _ [] = []
       | zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest
       | zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest
       | zip_vars [] _ = error "More instantiations than variables in theorem";
     val insts =
       zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
       zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
   in insts end;
 
 val inst =  Args.maybe Parse_Tools.name_term;
 val concl = Args.$$$ "concl" -- Args.colon;
 
 fun close_unchecked_insts context ((insts, concl_inst), fixes) =
   let
     val ctxt = Context.proof_of context;
     val ctxt1 = ctxt |> Proof_Context.add_fixes_cmd fixes |> #2;
 
     val insts' = insts @ concl_inst;
 
     val term_insts =
       map (the_list o (Option.map Parse_Tools.the_parse_val)) insts'
       |> burrow (Syntax.read_terms ctxt1 #> Variable.export_terms ctxt1 ctxt)
       |> map (try the_single);
 
     val _ =
       (insts', term_insts)
       |> ListPair.app (fn (SOME p, SOME t) => Parse_Tools.the_parse_fun p t | _ => ());
     val (insts'', concl_insts'') = chop (length insts) term_insts;
    in Unchecked_Term_Insts (insts'', concl_insts'') end;
 
 fun read_of_insts checked context ((insts, concl_insts), fixes) =
   if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
   then
     if checked
     then
       (fn _ =>
        Term_Insts
         (map (unembed_indexname o Parse_Tools.the_real_val) (map_filter I (insts @ concl_insts))))
     else
       (fn _ =>
         Unchecked_Term_Insts
           (map (Option.map Parse_Tools.the_real_val) insts,
             map (Option.map Parse_Tools.the_real_val) concl_insts))
   else
     if checked
     then
       (fn thm =>
         Named_Insts
           (apply2
             (map (Option.map (fn p => (Parse_Tools.the_parse_val p, Parse_Tools.the_parse_fun p))))
             (insts, concl_insts)
           |> of_rule thm |> map ((fn (xi, (nm, f)) => embed_indexname ((xi, nm), f))), fixes))
     else
       let val result = close_unchecked_insts context ((insts, concl_insts), fixes);
       in fn _ => result end;
 
 
 fun read_instantiate_closed ctxt (Named_Insts (insts, fixes)) thm  =
       let
         val insts' = map (fn ((v, t), _) => ((v, Position.none), t)) insts;
 
         val (thm_insts, thm') = add_thm_insts ctxt thm;
         val (thm'', thm_insts') =
           Rule_Insts.where_rule ctxt insts' fixes thm'
           |> get_thm_insts;
 
         val tyinst =
           ListPair.zip (fst thm_insts, fst thm_insts') |> map (fn ((xi, _), typ) => (xi, typ));
         val tinst =
           ListPair.zip (snd thm_insts, snd thm_insts') |> map (fn ((xi, _), t) => (xi, t));
 
         val _ =
           map (fn ((xi, _), f) =>
             (case AList.lookup (op =) tyinst xi of
               SOME typ => f (Logic.mk_type typ)
             | NONE =>
                 (case AList.lookup (op =) tinst xi of
                   SOME t => f t
                 | NONE => error "Lost indexname in instantiated theorem"))) insts;
       in
         (thm'' |> restore_tags thm)
       end
   | read_instantiate_closed ctxt (Unchecked_Term_Insts insts) thm =
       let
         val (xis, ts) = ListPair.unzip (of_rule thm insts);
         val ctxt' = Variable.declare_maxidx (Thm.maxidx_of thm) ctxt;
         val (ts', ctxt'') = Variable.import_terms false ts ctxt';
         val ts'' = Variable.export_terms ctxt'' ctxt ts';
         val insts' = ListPair.zip (xis, ts'');
       in instantiate_xis ctxt insts' thm end
   | read_instantiate_closed ctxt (Term_Insts insts) thm =
       instantiate_xis ctxt insts thm;
 
 val _ =
   Theory.setup
     (Attrib.setup \<^binding>\<open>where\<close>
       (Scan.lift
         (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
         >> (fn args =>
             let val args' = read_where_insts args in
               fn (context, thm) =>
                 (NONE, SOME (read_instantiate_closed (Context.proof_of context) args' thm))
             end))
       "named instantiation of theorem");
 
 val _ =
   Theory.setup
     (Attrib.setup \<^binding>\<open>of\<close>
       (Scan.lift
         (Args.mode "unchecked" --
           (Scan.repeat (Scan.unless concl inst) --
             Scan.optional (concl |-- Scan.repeat inst) [] --
             Parse.for_fixes)) -- Scan.state >>
       (fn ((unchecked, args), context) =>
         let
           val read_insts = read_of_insts (not unchecked) context args;
         in
           fn (context, thm) =>
             let val thm' =
               if Thm.is_free_dummy thm andalso unchecked
               then Drule.free_dummy_thm
               else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm
             in (NONE, SOME thm') end
         end))
       "positional instantiation of theorem");
 
 end;
diff --git a/src/HOL/Eisbach/match_method.ML b/src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML
+++ b/src/HOL/Eisbach/match_method.ML
@@ -1,749 +1,749 @@
 (*  Title:      HOL/Eisbach/match_method.ML
     Author:     Daniel Matichuk, NICTA/UNSW
 
 Setup for "match" proof method. It provides basic fact/term matching in
 addition to premise/conclusion matching through Subgoal.focus, and binds
 fact names from matches as well as term patterns within matches.
 *)
 
 signature MATCH_METHOD =
 sig
   val focus_schematics: Proof.context -> Envir.tenv
   val focus_params: Proof.context -> term list
   (* FIXME proper ML interface for the main thing *)
 end
 
 structure Match_Method : MATCH_METHOD =
 struct
 
 (* Filter premises by predicate, with premise order; recovers premise order afterwards.*)
 fun filter_prems_tac' ctxt prem =
   let
     fun Then NONE tac = SOME tac
       | Then (SOME tac) tac' = SOME (tac THEN' tac');
     fun thins idxH (tac, n, i) =
        if prem idxH then (tac, n + 1 , i)
        else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, i + n);
   in
     SUBGOAL (fn (goal, i) =>
       let val idxHs = tag_list 0 (Logic.strip_assums_hyp goal) in
         (case fold thins idxHs (NONE, 0, 0) of
           (NONE, _, _) => no_tac
         | (SOME tac, _, n) => tac i THEN rotate_tac (~ n) i)
       end)
   end;
 
 
 datatype match_kind =
     Match_Term of term Item_Net.T
   | Match_Fact of thm Item_Net.T
   | Match_Concl
   | Match_Prems of bool;
 
 
 val aconv_net = Item_Net.init (op aconv) single;
 
 val parse_match_kind =
   Scan.lift \<^keyword>\<open>conclusion\<close> >> K Match_Concl ||
   Scan.lift (\<^keyword>\<open>premises\<close> |-- Args.mode "local") >> Match_Prems ||
   Scan.lift (\<^keyword>\<open>(\<close>) |-- Args.term --| Scan.lift (\<^keyword>\<open>)\<close>) >>
     (fn t => Match_Term (Item_Net.update t aconv_net)) ||
   Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules));
 
 
 fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems _ => true | _ => false);
 fun prop_match m = (case m of Match_Term _ => false | _ => true);
 
 val bound_thm : (thm, binding) Parse_Tools.parse_val parser =
   Parse_Tools.parse_thm_val Parse.binding;
 
 val bound_term : (term, binding) Parse_Tools.parse_val parser =
   Parse_Tools.parse_term_val Parse.binding;
 
 val fixes =
   Parse.and_list1 (Scan.repeat1 (Parse.position bound_term) --
     Scan.option (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.typ)
     >> (fn (xs, T) => map (fn (x, pos) => ((x, T), pos)) xs)) >> flat;
 
 val for_fixes = Scan.optional (\<^keyword>\<open>for\<close> |-- fixes) [];
 
 fun pos_of dyn = Parse_Tools.the_parse_val dyn |> Binding.pos_of;
 
 (*FIXME: Dynamic facts modify the background theory, so we have to resort
   to token replacement for matched facts. *)
 val dynamic_fact =
   Scan.lift bound_thm -- Attrib.opt_attribs;
 
 type match_args = {multi : bool, cut : int};
 
 val parse_match_args =
   Scan.optional
     (Args.parens
       (Parse.enum1 ","
         (Args.$$$ "multi" >> (fn _ => fn {cut, ...} => {multi = true, cut = cut}) ||
          Args.$$$ "cut" |-- Scan.optional Parse.nat 1
           >> (fn n => fn {multi, ...} => {multi = multi, cut = n})))) []
   >> (fn fs => fold I fs {multi = false, cut = ~1});
 
 fun parse_named_pats match_kind =
   Args.context --
   Parse.and_list1'
     (Scan.option (dynamic_fact --| Scan.lift Args.colon) :--
       (fn opt_dyn =>
         if is_none opt_dyn orelse nameable_match match_kind
         then Scan.lift (Parse_Tools.name_term -- parse_match_args)
         else
           let val b = #1 (the opt_dyn)
           in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end)) --
   Scan.lift (for_fixes -- (\<^keyword>\<open>\<Rightarrow>\<close> |-- Parse.token Parse.text))
   >> (fn ((ctxt, ts), (fixes, body)) =>
     (case Token.get_value body of
       SOME (Token.Source src) =>
         let
           val text = Method.read ctxt src;
           val ts' =
             map
               (fn (b, (Parse_Tools.Real_Val v, match_args)) =>
                 ((Option.map (fn (b, att) =>
                   (Parse_Tools.the_real_val b, att)) b, match_args), v)
                 | _ => raise Fail "Expected closed term") ts
           val fixes' = map (fn ((p, _), _) => Parse_Tools.the_real_val p) fixes
         in (ts', fixes', text) end
     | _ =>
         let
           val (fix_names, ctxt3) = ctxt
             |> Proof_Context.add_fixes_cmd
               (map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes)
             ||> Proof_Context.set_mode Proof_Context.mode_schematic;
 
           fun parse_term term =
             if prop_match match_kind
             then Syntax.parse_prop ctxt3 term
             else Syntax.parse_term ctxt3 term;
 
           fun drop_judgment_dummy t =
             (case t of
               Const (judgment, _) $
                 (Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $
                   Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, _)) =>
                 if judgment = Object_Logic.judgment_name ctxt then
                     Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $
                       Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, propT)
                 else t
             | t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2
             | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b)
             | _ => t);
 
           val pats =
             map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
             |> map drop_judgment_dummy
             |> (fn ts => fold_map Term.replace_dummy_patterns ts (Variable.maxidx_of ctxt3 + 1))
             |> fst
             |> Syntax.check_terms ctxt3;
 
           val pat_fixes = fold (Term.add_frees) pats [] |> map fst;
 
           val _ =
             map2 (fn nm => fn (_, pos) =>
                 member (op =) pat_fixes nm orelse
                 error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
               fix_names fixes;
 
           val _ = map (Term.map_types Type.no_tvars) pats;
 
           val ctxt4 = fold Variable.declare_term pats ctxt3;
 
           val (real_fixes, ctxt5) = ctxt4
             |> fold_map Proof_Context.inferred_param fix_names |>> map Free;
 
           fun reject_extra_free (Free (x, _)) () =
                 if Variable.is_fixed ctxt5 x then ()
                 else error ("Illegal use of free (unfixed) variable " ^ quote x)
             | reject_extra_free _ () = ();
           val _ = (fold o fold_aterms) reject_extra_free pats ();
 
           val binds =
             map (fn (b, _) => Option.map (fn (b, att) => (Parse_Tools.the_parse_val b, att)) b) ts;
 
           fun upd_ctxt (SOME (b, att)) pat (tms, ctxt) =
                 let
                   val ([nm], ctxt') =
                     Variable.variant_fixes [Name.internal (Binding.name_of b)] ctxt;
                   val abs_nms = Term.strip_all_vars pat;
 
                   val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
                     |> Conjunction.intr_balanced
                     |> Drule.generalize ([], map fst abs_nms)
                     |> Thm.tag_free_dummy;
 
                   val atts = map (Attrib.attribute ctxt') att;
                   val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
 
                   fun label_thm thm =
                     Thm.cterm_of ctxt'' (Free (nm, propT))
                     |> Drule.mk_term
                     |> not (null abs_nms) ? Conjunction.intr thm
 
                   val [head_thm, body_thm] =
                     Drule.zero_var_indexes_list (map label_thm [param_thm, param_thm'])
                     |> map Thm.tag_free_dummy;
 
                   val ctxt''' =
                     Attrib.local_notes "" [((b, []), [([body_thm], [])])] ctxt''
                     |> snd
                     |> Variable.declare_maxidx (Thm.maxidx_of head_thm);
                 in
                   (SOME (head_thm, att) :: tms, ctxt''')
                 end
             | upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt);
 
           val (binds, ctxt6) = ctxt5
             |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
             ||> Proof_Context.restore_mode ctxt;
 
           val (text, src) = Method.read_closure_input ctxt6 (Token.input_of body);
 
           val morphism =
             Variable.export_morphism ctxt6
               (ctxt
                 |> fold Token.declare_maxidx src
                 |> Variable.declare_maxidx (Variable.maxidx_of ctxt6));
 
           val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats;
           val _ = ListPair.app (fn ((_, (v, _)), t) => Parse_Tools.the_parse_fun v t) (ts, pats');
 
           fun close_src src =
             let
               val src' = src |> map (Token.closure #> Token.transform morphism);
               val _ =
                 (Token.args_of_src src ~~ Token.args_of_src src')
                 |> List.app (fn (tok, tok') =>
                   (case Token.get_value tok' of
                     SOME value => ignore (Token.assign (SOME value) tok)
                   | NONE => ()));
             in src' end;
 
           val binds' =
             map (Option.map (fn (t, atts) => (Morphism.thm morphism t, map close_src atts))) binds;
 
           val _ =
             ListPair.app
               (fn ((SOME ((v, _)), _), SOME (t, _)) => Parse_Tools.the_parse_fun v t
                 | ((NONE, _), NONE) => ()
                 | _ => error "Mismatch between real and parsed bound variables")
               (ts, binds');
 
           val real_fixes' = map (Morphism.term morphism) real_fixes;
           val _ =
             ListPair.app (fn (((v, _) , _), t) => Parse_Tools.the_parse_fun v t)
               (fixes, real_fixes');
 
           val match_args = map (fn (_, (_, match_args)) => match_args) ts;
           val binds'' = (binds' ~~ match_args) ~~ pats';
 
           val src' = map (Token.transform morphism) src;
           val _ = Token.assign (SOME (Token.Source src')) body;
         in
           (binds'', real_fixes', text)
         end));
 
 
 fun dest_internal_term t =
   (case try Logic.dest_conjunction t of
     SOME (params, head) =>
      (params |> Logic.dest_conjunctions |> map Logic.dest_term,
       head |> Logic.dest_term)
   | NONE => ([], t |> Logic.dest_term));
 
 fun dest_internal_fact thm = dest_internal_term (Thm.prop_of thm);
 
 fun inst_thm ctxt env ts params thm =
   let
     val ts' = map (Envir.norm_term env) ts;
     val insts = map (#1 o dest_Var) ts' ~~ map (Thm.cterm_of ctxt) params;
   in infer_instantiate ctxt insts thm end;
 
 fun do_inst fact_insts' env text ctxt =
   let
     val fact_insts =
       map_filter
         (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att))
           | _ => NONE) fact_insts';
 
-    fun try_dest_term thm = try (dest_internal_fact #> snd) thm;
+    fun try_dest_term thm = \<^try>\<open>#2 (dest_internal_fact thm)\<close>;
 
     fun expand_fact fact_insts thm =
       the_default [thm]
         (case try_dest_term thm of
           SOME t_ident => AList.lookup (op aconv) fact_insts t_ident
         | NONE => NONE);
 
     fun fact_morphism fact_insts =
       Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $>
       Morphism.typ_morphism "do_inst.type" (Envir.norm_type (Envir.type_env env)) $>
       Morphism.fact_morphism "do_inst.fact" (maps (expand_fact fact_insts));
 
     fun apply_attribute (head, (fact, atts)) (fact_insts, ctxt) =
       let
         val morphism = fact_morphism fact_insts;
         val atts' = map (Attrib.attribute ctxt o map (Token.transform morphism)) atts;
         val (fact'', ctxt') = fold_map (Thm.proof_attributes atts') fact ctxt;
       in ((head, fact'') :: fact_insts, ctxt') end;
 
      (*TODO: What to do about attributes that raise errors?*)
     val (fact_insts', ctxt') = fold_rev (apply_attribute) fact_insts ([], ctxt);
 
     val text' = (Method.map_source o map) (Token.transform (fact_morphism fact_insts')) text;
   in
     (text', ctxt')
   end;
 
 fun prep_fact_pat ((x, args), pat) ctxt =
   let
     val ((params, pat'), ctxt') = Variable.focus NONE pat ctxt;
     val params' = map (Free o snd) params;
 
     val morphism =
       Variable.export_morphism ctxt'
         (ctxt |> Variable.declare_maxidx (Variable.maxidx_of ctxt'));
     val pat'' :: params'' = map (Morphism.term morphism) (pat' :: params');
 
     fun prep_head (t, att) = (dest_internal_fact t, att);
   in
     ((((Option.map prep_head x, args), params''), pat''), ctxt')
   end;
 
 fun morphism_env morphism env =
   let
     val tenv = Envir.term_env env
       |> Vartab.map (K (fn (T, t) => (Morphism.typ morphism T, Morphism.term morphism t)));
     val tyenv = Envir.type_env env
       |> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T)));
    in Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv, tyenv = tyenv} end;
 
 fun export_with_params ctxt morphism (SOME ts, params) thm env =
       let
         val outer_env = morphism_env morphism env;
         val thm' = Morphism.thm morphism thm;
       in inst_thm ctxt outer_env params ts thm' end
   | export_with_params _ morphism (NONE, _) thm _ = Morphism.thm morphism thm;
 
 fun match_filter_env is_newly_fixed pat_vars fixes params env =
   let
     val param_vars = map Term.dest_Var params;
 
     val tenv = Envir.term_env env;
     val params' = map (fn (xi, _) => Vartab.lookup tenv xi) param_vars;
 
     val fixes_vars = map Term.dest_Var fixes;
 
     val all_vars = Vartab.keys tenv;
     val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
 
     val tenv' = tenv |> fold (Vartab.delete_safe) extra_vars;
     val env' =
       Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env};
 
     val all_params_bound = forall (fn SOME (_, Free (x, _)) => is_newly_fixed x | _ => false) params';
     val all_params_distinct = not (has_duplicates (eq_option (eq_pair (op =) (op aconv))) params');
 
     val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
     val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes;
   in
     if all_params_bound andalso all_pat_fixes_bound andalso all_params_distinct
     then SOME env'
     else NONE
   end;
 
 
 (* Slightly hacky way of uniquely identifying focus premises *)
 val prem_idN = "premise_id";
 
 fun prem_id_eq ((id, _ : thm), (id', _ : thm)) = id = id';
 
 val prem_rules : (int * thm) Item_Net.T =
   Item_Net.init prem_id_eq (single o Thm.full_prop_of o snd);
 
 fun raw_thm_to_id thm =
   (case Properties.get (Thm.get_tags thm) prem_idN of NONE => NONE | SOME id => Int.fromString id)
   |> the_default ~1;
 
 structure Focus_Data = Proof_Data
 (
   type T =
     (int * (int * thm) Item_Net.T) *  (*prems*)
     Envir.tenv *  (*schematics*)
     term list  (*params*)
   fun init _ : T = ((0, prem_rules), Vartab.empty, [])
 );
 
 
 (* focus prems *)
 
 val focus_prems = #1 o Focus_Data.get;
 
 fun transfer_focus_prems from_ctxt =
   Focus_Data.map (@{apply 3(1)} (K (focus_prems from_ctxt)))
 
 
 fun add_focus_prem prem =
   `(Focus_Data.get #> #1 #> #1) ##>
   (Focus_Data.map o @{apply 3(1)}) (fn (next, net) =>
     (next + 1, Item_Net.update (next, Thm.tag_rule (prem_idN, string_of_int next) prem) net));
 
 fun remove_focus_prem' (ident, thm) =
   (Focus_Data.map o @{apply 3(1)} o apsnd)
     (Item_Net.remove (ident, thm));
 
 fun remove_focus_prem thm = remove_focus_prem' (raw_thm_to_id thm, thm);
 
 (*TODO: Preliminary analysis to see if we're trying to clear in a non-focus match?*)
 val _ =
   Theory.setup
     (Attrib.setup \<^binding>\<open>thin\<close>
       (Scan.succeed
         (Thm.declaration_attribute (fn th => Context.mapping I (remove_focus_prem th))))
         "clear premise inside match method");
 
 
 (* focus schematics *)
 
 val focus_schematics = #2 o Focus_Data.get;
 
 fun add_focus_schematics schematics =
   (Focus_Data.map o @{apply 3(2)})
     (fold (fn ((xi, T), ct) => Vartab.update_new (xi, (T, Thm.term_of ct))) schematics);
 
 
 (* focus params *)
 
 val focus_params = #3 o Focus_Data.get;
 
 fun add_focus_params params =
   (Focus_Data.map o @{apply 3(3)})
     (append (map (fn (_, ct) => Thm.term_of ct) params));
 
 
 (* Add focus elements as proof data *)
 fun augment_focus (focus: Subgoal.focus) : (int list * Subgoal.focus) =
   let
     val {context, params, prems, asms, concl, schematics} = focus;
 
     val (prem_ids, ctxt') = context
       |> add_focus_params params
       |> add_focus_schematics (snd schematics)
       |> fold_map add_focus_prem (rev prems)
 
   in
     (prem_ids,
       {context = ctxt',
        params = params,
        prems = prems,
        concl = concl,
        schematics = schematics,
        asms = asms})
   end;
 
 
 (* Fix schematics in the goal *)
 fun focus_concl ctxt i bindings goal =
   let
     val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
       Subgoal.focus_params ctxt i bindings goal;
 
     val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
     val schematic_terms = map (apsnd (Thm.cterm_of ctxt'')) (#2 inst);
 
     val goal'' = Thm.instantiate ([], schematic_terms) goal';
     val concl' = Thm.instantiate_cterm ([], schematic_terms) concl;
     val (schematic_types, schematic_terms') = schematics;
     val schematics' = (schematic_types, schematic_terms @ schematic_terms');
   in
     ({context = ctxt'', concl = concl', params = params, prems = prems,
       schematics = schematics', asms = asms} : Subgoal.focus, goal'')
   end;
 
 
 fun deduplicate eq prev seq =
   Seq.make (fn () =>
     (case Seq.pull seq of
       SOME (x, seq') =>
         if member eq prev x
         then Seq.pull (deduplicate eq prev seq')
         else SOME (x, deduplicate eq (x :: prev) seq')
     | NONE => NONE));
 
 
 fun consistent_env env =
   let
     val tenv = Envir.term_env env;
     val tyenv = Envir.type_env env;
   in
     forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
   end;
 
 fun term_eq_wrt (env1, env2) (t1, t2) =
   Envir.eta_contract (Envir.norm_term env1 t1) aconv
   Envir.eta_contract (Envir.norm_term env2 t2);
 
 fun type_eq_wrt (env1, env2) (T1, T2) =
   Envir.norm_type (Envir.type_env env1) T1 = Envir.norm_type (Envir.type_env env2) T2;
 
 
 fun eq_env (env1, env2) =
     Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso
     ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) =>
         (var = var' andalso term_eq_wrt (env1, env2) (t, t')))
       (apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2))
     andalso
     ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) =>
         var = var' andalso type_eq_wrt (env1, env2) (T, T'))
       (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2));
 
 
 fun merge_env (env1, env2) =
   let
     val tenv =
       Vartab.merge (eq_snd (term_eq_wrt (env1, env2))) (Envir.term_env env1, Envir.term_env env2);
     val tyenv =
       Vartab.merge (eq_snd (type_eq_wrt (env1, env2)) andf eq_fst (op =))
         (Envir.type_env env1, Envir.type_env env2);
     val maxidx = Int.max (Envir.maxidx_of env1, Envir.maxidx_of env2);
   in Envir.Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv} end;
 
 
 fun import_with_tags thms ctxt =
   let
     val ((_, thms'), ctxt') = Variable.import false thms ctxt;
     val thms'' = map2 (fn thm => Thm.map_tags (K (Thm.get_tags thm))) thms thms';
   in (thms'', ctxt') end;
 
 
 fun try_merge (env, env') = SOME (merge_env (env, env')) handle Vartab.DUP _ => NONE
 
 
 fun Seq_retrieve seq f =
   let
     fun retrieve' (list, seq) f =
       (case Seq.pull seq of
         SOME (x, seq') =>
           if f x then (SOME x, (list, seq'))
           else retrieve' (list @ [x], seq') f
       | NONE => (NONE, (list, seq)));
 
     val (result, (list, seq)) = retrieve' ([], seq) f;
   in (result, Seq.append (Seq.of_list list) seq) end;
 
 fun match_facts ctxt fixes prop_pats get =
   let
     fun is_multi (((_, x : match_args), _), _) = #multi x;
     fun get_cut (((_, x : match_args), _), _) = #cut x;
     fun do_cut n = if n = ~1 then I else Seq.take n;
 
     val raw_thmss = map (get o snd) prop_pats;
     val (thmss, ctxt') = fold_burrow import_with_tags raw_thmss ctxt;
 
     val newly_fixed = Variable.is_newly_fixed ctxt' ctxt;
 
     val morphism = Variable.export_morphism ctxt' ctxt;
 
     fun match_thm (((x, params), pat), thm)  =
       let
         val pat_vars = Term.add_vars pat [];
 
         val ts = Option.map (fst o fst) (fst x);
 
         val item' = Thm.prop_of thm;
 
         val matches =
           (Unify.matchers (Context.Proof ctxt) [(pat, item')])
           |> Seq.filter consistent_env
           |> Seq.map_filter (fn env' =>
               (case match_filter_env newly_fixed pat_vars fixes params env' of
                 SOME env'' => SOME (export_with_params ctxt morphism (ts, params) thm env', env'')
               | NONE => NONE))
           |> Seq.map (apfst (Thm.map_tags (K (Thm.get_tags thm))))
           |> deduplicate (eq_pair Thm.eq_thm_prop eq_env) []
       in matches end;
 
     val all_matches =
       map2 pair prop_pats thmss
       |> map (fn (pat, matches) => (pat, map (fn thm => match_thm (pat, thm)) matches));
 
     fun proc_multi_match (pat, thmenvs) (pats, env) =
       do_cut (get_cut pat)
         (if is_multi pat then
           let
             fun maximal_set tail seq envthms =
               Seq.make (fn () =>
                 (case Seq.pull seq of
                   SOME ((thm, env'), seq') =>
                     let
                       val (result, envthms') =
                         Seq_retrieve envthms (fn (env, _) => eq_env (env, env'));
                     in        
                       (case result of
                         SOME (_, thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms')
                       | NONE => Seq.pull (maximal_set (tail @ [(env', [thm])]) seq' envthms'))
                     end
                  | NONE => Seq.pull (Seq.append envthms (Seq.of_list tail))));
 
             val maximal_sets = fold (maximal_set []) thmenvs Seq.empty;
           in
             maximal_sets
             |> Seq.map swap
             |> Seq.filter (fn (thms, _) => not (null thms))
             |> Seq.map_filter (fn (thms, env') =>
               (case try_merge (env, env') of
                 SOME env'' => SOME ((pat, thms) :: pats, env'')
               | NONE => NONE))
           end
         else
           let
             fun just_one (thm, env') =
               (case try_merge (env, env') of
                 SOME env'' => SOME ((pat, [thm]) :: pats, env'')
               | NONE => NONE);
           in fold (fn seq => Seq.append (Seq.map_filter just_one seq)) thmenvs Seq.empty end);
 
     val all_matches =
       Seq.EVERY (map proc_multi_match all_matches) ([], Envir.init);
   in
     all_matches
     |> Seq.map (apsnd (morphism_env morphism))
   end;
 
 fun real_match using outer_ctxt fixes m text pats st =
   let              
     val goal_ctxt =
       fold Variable.declare_term fixes outer_ctxt
       (*FIXME Is this a good idea? We really only care about the maxidx*)
       |> fold (fn (_, t) => Variable.declare_term t) pats;
 
     fun make_fact_matches ctxt get =
       let
         val (pats', ctxt') = fold_map prep_fact_pat pats ctxt;
       in
         match_facts ctxt' fixes pats' get
         |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt')
       end;
 
     fun make_term_matches ctxt get =
       let
         val pats' = map
           (fn ((SOME _, _), _) => error "Cannot name term match"
             | ((_, x), t) => (((NONE, x), []), Logic.mk_term t)) pats;
 
         val thm_of = Drule.mk_term o Thm.cterm_of ctxt;
         fun get' t = get (Logic.dest_term t) |> map thm_of;
       in
         match_facts ctxt fixes pats' get'
         |> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt)
       end;
   in
     (case m of
       Match_Fact net =>
         make_fact_matches goal_ctxt (Item_Net.retrieve net)
         |> Seq.map (fn (text, ctxt') =>
           Method.evaluate_runtime text ctxt' using (ctxt', st)
           |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
     | Match_Term net =>
         make_term_matches goal_ctxt (Item_Net.retrieve net)
         |> Seq.map (fn (text, ctxt') =>
           Method.evaluate_runtime text ctxt' using (ctxt', st)
           |> Seq.filter_results |> Seq.map (fn (_, thm) => (outer_ctxt, thm)))
     | match_kind =>
         if Thm.no_prems st then Seq.empty
         else
           let
             fun focus_cases f g =
               (case match_kind of
                 Match_Prems b => f b
               | Match_Concl => g
               | _ => raise Fail "Match kind fell through");
 
             val ((local_premids, {context = focus_ctxt, params, asms, concl, prems, ...}), focused_goal) =
               focus_cases (K Subgoal.focus_prems) focus_concl goal_ctxt 1 NONE st
               |>> augment_focus;
             
             val texts =
               focus_cases
                 (fn is_local => fn _ =>
                   make_fact_matches focus_ctxt
                     (Item_Net.retrieve (focus_prems focus_ctxt |> snd)
                      #> is_local ? filter (fn (p, _) => exists (fn id' => id' = p) local_premids)
                      #> order_list))
                 (fn _ =>
                   make_term_matches focus_ctxt
                     (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)]))
                 ();
 
             (*TODO: How to handle cases? *)
 
             fun do_retrofit (inner_ctxt, st1) =
               let
                 val (_, before_prems) = focus_prems focus_ctxt;
                 val (_, after_prems) = focus_prems inner_ctxt;
 
                 val removed_prems =
                   Item_Net.filter (null o Item_Net.lookup after_prems) before_prems
 
                 val removed_local_prems = Item_Net.content removed_prems
                   |> filter (fn (id, _) => member (op =) local_premids id)
                   |> map (fn (_, prem) => Thm.prop_of prem)
 
                 fun filter_removed_prems prems =
                   Item_Net.filter (null o Item_Net.lookup removed_prems) prems;
                                      
                 val outer_ctxt' = outer_ctxt 
                   |> Focus_Data.map (@{apply 3(1)} (apsnd filter_removed_prems));
 
                 val n_subgoals = Thm.nprems_of st1;
 
                 val removed_prem_idxs = 
                   prems
                   |> tag_list 0
                   |> filter (member (op aconv) removed_local_prems o Thm.prop_of o snd)
                   |> map fst
 
                 fun filter_prem (i, _) = not (member (op =) removed_prem_idxs i); 
 
               in
                 Subgoal.retrofit inner_ctxt goal_ctxt params asms 1 st1 st
                 |> focus_cases 
                    (fn _ => (n_subgoals > 0 andalso length removed_local_prems > 0) ?
                     (Seq.map (Goal.restrict 1 n_subgoals)
                       #> Seq.maps (ALLGOALS (fn i =>
                           DETERM (filter_prems_tac' goal_ctxt filter_prem i)))
                       #> Seq.map (Goal.unrestrict 1)))
                    I
                 |> Seq.map (pair outer_ctxt')
               end;
 
             fun apply_text (text, ctxt') =
                 Method.evaluate_runtime text ctxt' using (ctxt', focused_goal)
               |> Seq.filter_results
               |> Seq.maps (Seq.DETERM do_retrofit)             
 
           in Seq.map apply_text texts end)
   end;
 
 val _ =
   Theory.setup
     (Method.setup \<^binding>\<open>match\<close>
       (parse_match_kind :--
         (fn kind => Scan.lift \<^keyword>\<open>in\<close> |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
         (fn (matches, bodies) => fn ctxt =>
           CONTEXT_METHOD (fn using => Method.RUNTIME (fn (goal_ctxt, st) =>
             let
               val ctxt' = transfer_focus_prems goal_ctxt ctxt;
               fun exec (pats, fixes, text) st' =
                 real_match using ctxt' fixes matches text pats st';
             in
               Seq.flat (Seq.FIRST (map exec bodies) st)
               |> Seq.map (apfst (fn ctxt' => transfer_focus_prems ctxt' goal_ctxt))
               |> Seq.make_results
             end))))
       "structural analysis/matching on goals");
 
 end;