# HG changeset patch
# User wenzelm
# Date 1431770752 -7200
# Node ID b4f1a0a701ae39e1ed9e39dd9bf9a2e43cca9e4a
# Parent  014b86186c49a5f7f2f1d707e0265caa8a486015
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;

diff -r 014b86186c49 -r b4f1a0a701ae src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy	Sat May 16 12:05:52 2015 +0200
@@ -17,16 +17,16 @@
 begin
 
 ML_file "parse_tools.ML"
+ML_file "method_closure.ML"
 ML_file "eisbach_rule_insts.ML"
-ML_file "method_closure.ML"
 ML_file "match_method.ML"
 ML_file "eisbach_antiquotations.ML"
 
 (* FIXME reform Isabelle/Pure attributes to make this work by default *)
 setup \<open>
-  fold (Method_Closure.wrap_attribute true)
+  fold (Method_Closure.wrap_attribute {handle_all_errs = true, declaration = true})
     [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
-  fold (Method_Closure.wrap_attribute false)
+  fold (Method_Closure.wrap_attribute {handle_all_errs = false, declaration = false})
     [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
 \<close>
 
diff -r 014b86186c49 -r b4f1a0a701ae src/HOL/Eisbach/Eisbach_Tools.thy
--- a/src/HOL/Eisbach/Eisbach_Tools.thy	Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Sat May 16 12:05:52 2015 +0200
@@ -45,4 +45,37 @@
 end
 \<close>
 
+ML \<open>
+  fun try_map v seq =
+    (case try Seq.pull seq of
+      SOME (SOME (x, seq')) => Seq.make (fn () => SOME(x, try_map v seq'))
+    | SOME NONE => Seq.empty
+    | NONE => v);
+\<close>
+
+method_setup catch = \<open>
+  Method_Closure.parse_method -- Method_Closure.parse_method >>
+    (fn (text, text') => fn ctxt => fn using => fn st =>
+      let
+        val method = Method_Closure.method_evaluate text ctxt using;
+        val backup_results = Method_Closure.method_evaluate text' ctxt using st;
+      in
+        (case try method st of
+          SOME seq => try_map backup_results seq
+        | NONE => backup_results)
+      end)
+\<close>
+
+ML \<open>
+  fun uncurry_rule thm = Conjunction.uncurry_balanced (Thm.nprems_of thm) thm;
+  fun curry_rule thm =
+    if Thm.no_prems thm then thm
+    else
+      let val conjs = Logic.dest_conjunctions (Thm.major_prem_of thm);
+      in Conjunction.curry_balanced (length conjs) thm end;
+\<close>
+
+attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute (K uncurry_rule))\<close>
+attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute (K curry_rule))\<close>
+
 end
diff -r 014b86186c49 -r b4f1a0a701ae src/HOL/Eisbach/Examples.thy
--- a/src/HOL/Eisbach/Examples.thy	Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/Examples.thy	Sat May 16 12:05:52 2015 +0200
@@ -68,8 +68,7 @@
   (match conclusion in
     "P \<and> Q" for P Q \<Rightarrow>
       \<open>print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption\<close>
-    \<bar> "H" for H \<Rightarrow> \<open>print_term H\<close>
-  )
+    \<bar> "H" for H \<Rightarrow> \<open>print_term H\<close>)
 
 text \<open>Solves goal\<close>
 lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q"
@@ -149,15 +148,13 @@
 
 subsection \<open>Demo\<close>
 
-method solve methods m = (m; fail)
-
 named_theorems intros and elims and subst
 
 method prop_solver declares intros elims subst =
   (assumption |
     rule intros | erule elims |
     subst subst | subst (asm) subst |
-    (erule notE; solve \<open>prop_solver\<close>))+
+    (erule notE; solves \<open>prop_solver\<close>))+
 
 lemmas [intros] =
   conjI
@@ -187,7 +184,7 @@
   done
 
 lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow>  P z \<Longrightarrow> P y \<Longrightarrow> Q y"
-  apply (solve \<open>guess_all, prop_solver\<close>)  -- \<open>Try it without solve\<close>
+  apply (solves \<open>guess_all, prop_solver\<close>)  -- \<open>Try it without solve\<close>
   done
 
 method guess_ex =
@@ -202,7 +199,7 @@
   done
 
 method fol_solver =
-  ((guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>)
+  ((guess_ex | guess_all | prop_solver) ; solves \<open>fol_solver\<close>)
 
 declare
   allI [intros]
@@ -215,4 +212,36 @@
   and "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)"
   by fol_solver+
 
+
+text \<open>
+  Eisbach_Tools provides the catch method, which catches run-time method
+  errors. In this example the OF attribute throws an error when it can't
+  compose H with A, forcing H to be re-bound to different members of imps
+  until it succeeds.
+\<close>
+
+lemma
+  assumes imps:  "A \<Longrightarrow> B" "A \<Longrightarrow> C" "B \<Longrightarrow> D"
+  assumes A: "A"
+  shows "B \<and> C"
+  apply (rule conjI)
+  apply ((match imps in H:"_ \<Longrightarrow> _" \<Rightarrow> \<open>catch \<open>rule H[OF A], print_fact H\<close> \<open>print_fact H, fail\<close>\<close>)+)
+  done
+
+text \<open>
+  Eisbach_Tools provides the curry and uncurry attributes. This is useful
+  when the number of premises of a thm isn't known statically. The pattern
+  @{term "P \<Longrightarrow> Q"} matches P against the major premise of a thm, and Q is the
+  rest of the premises with the conclusion. If we first uncurry, then @{term
+  "P \<Longrightarrow> Q"} will match P with the conjunction of all the premises, and Q with
+  the final conclusion of the rule.
+\<close>
+
+lemma
+  assumes imps: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" "E \<Longrightarrow> D \<Longrightarrow> A"
+  shows "(A \<longrightarrow> B \<longrightarrow> C) \<and> (D \<longrightarrow> C)"
+    by (match imps[uncurry] in H[curry]:"_ \<Longrightarrow> C" (cut, multi) \<Rightarrow>
+                    \<open>match H in "E \<Longrightarrow> _" \<Rightarrow> \<open>fail\<close>
+                                      \<bar> _ \<Rightarrow> \<open>simp add: H\<close>\<close>)
+
 end
diff -r 014b86186c49 -r b4f1a0a701ae src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy	Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Sat May 16 12:05:52 2015 +0200
@@ -9,8 +9,7 @@
 begin
 
 
-
-section \<open>Named Theorems Tests\<close>
+subsection \<open>Named Theorems Tests\<close>
 
 named_theorems foo
 
@@ -22,8 +21,10 @@
   apply foo
   done
 
+method abs_used for P = (match (P) in "\<lambda>a. ?Q" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
 
-section \<open>Match Tests\<close>
+
+subsection \<open>Match Tests\<close>
 
 notepad
 begin
@@ -75,7 +76,8 @@
     apply (intro conjI)
     apply (match premises in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>)
     apply (match premises in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>\<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> Y': "?H" \<Rightarrow> \<open>-\<close>)\<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> \<open>fail\<close> \<bar> Y': _ \<Rightarrow> \<open>-\<close>)\<close>)\<close>)*)
     apply assumption
     done
 
@@ -106,16 +108,41 @@
     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>intro conjI Y[THEN conjunct1]\<close>)
+    apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow>
+                                  \<open>match (P) in B \<Rightarrow> \<open>fail\<close>
+                                        \<bar> "\<lambda>a. B" \<Rightarrow> \<open>fail\<close>
+                                        \<bar> _ \<Rightarrow> \<open>-\<close>,
+                                  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> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>)
+    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)"
@@ -145,6 +172,10 @@
     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)
@@ -156,13 +187,39 @@
   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>
+    by (match X in H: "A \<and> ?H" (multi, cut) \<Rightarrow>
           \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> \<open>fail\<close>\<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> \<open>fail\<close>
+                                         \<bar> _ \<Rightarrow> \<open>-\<close>\<close>
+                      ,match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>\<close>)
+    apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow> \<open>fail\<close>
+                              \<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> \<open>fail\<close>
+                                  \<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.*)
@@ -193,7 +250,8 @@
   fun test_internal_fact ctxt factnm =
     (case try (Proof_Context.get_thms ctxt) factnm of
       NONE => ()
-    | SOME _ => error "Found internal fact")\<close>
+    | SOME _ => error "Found internal fact");
+\<close>
 
 method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses)
 
@@ -205,7 +263,7 @@
 ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close>
 
 
-(* Testing term and fact passing in recursion *)
+subsection \<open>Testing term and fact passing in recursion\<close>
 
 method recursion_example for x :: bool uses facts =
   (match (x) in
@@ -219,6 +277,23 @@
   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> \<open>-\<close>
+  \<bar> "PROP ?P" \<Rightarrow> \<open>fail\<close>)
+
+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)
@@ -265,13 +340,14 @@
 
 
 
-(* Polymorphism test *)
+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
+lemmas my_thms = foo'_ax1 foo'_ax2 foo'_ax3
 
 definition first_id where "first_id x = x"
 
@@ -294,6 +370,36 @@
   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
 (
@@ -324,34 +430,36 @@
 end
 
 
-notepad begin
+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>)
+    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
-  
+    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
+    apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
+    done
 end
 
-(* Method name internalization test *)
+
+subsection \<open>Method name internalization test\<close>
 
 method test2 = (simp)
 
diff -r 014b86186c49 -r b4f1a0a701ae src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Sat May 16 12:05:52 2015 +0200
@@ -72,39 +72,59 @@
     |> restore_tags thm
   end;
 
+(* FIXME unused *)
+fun read_instantiate_no_thm ctxt insts fixes =
+  let
+    val (type_insts, term_insts) =
+      List.partition (fn (((x, _) : indexname), _) => String.isPrefix "'" x) insts;
+
+    val ctxt1 =
+      ctxt
+      |> Context_Position.not_really
+      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+
+    val typs =
+      map snd type_insts
+      |> Syntax.read_typs ctxt1
+      |> Syntax.check_typs ctxt1;
+
+    val typ_insts' = map2 (fn (xi, _) => fn T => (xi,T)) type_insts typs;
+
+    val terms =
+      map snd term_insts
+      |> Syntax.read_terms ctxt1
+      |> Syntax.check_terms ctxt1;
+
+    val term_insts' = map2 (fn (xi, _) => fn t => (xi, t)) term_insts terms;
+
+  in (typ_insts',term_insts') end;
+
 
 datatype rule_inst =
-  Named_Insts of ((indexname * string) * (term -> unit)) list
-| Term_Insts of (indexname * term) list;
+  Named_Insts of ((indexname * string) * (term -> unit)) list * (binding * string option * mixfix) list
+(*| Unchecked_Of_Insts of (string option list * string option 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 =
-      Logic.mk_conjunction (Logic.mk_term (Var (xi, fastype_of t)), Logic.mk_term t);
+  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 =
-  let
-    val (t, t') = apply2 Logic.dest_term (Logic.dest_conjunction t);
-    val (xi, _) = Term.dest_Var t;
-  in (xi, t') end;
+fun unembed_indexname t = dest_pair t |> apfst (Term.dest_Var #> fst);
 
-fun read_where_insts toks =
+fun read_where_insts (insts, fixes) =
   let
-    val parser =
-      Parse.!!!
-        (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
-          --| Scan.ahead Parse.eof;
-    val (insts, fixes) = the (Scan.read Token.stopper parser toks);
-
     val insts' =
       if forall (fn (_, v) => Parse_Tools.is_real_val v) insts
-      then Term_Insts (map (fn (_, t) => unembed_indexname (Parse_Tools.the_real_val t)) insts)
-      else Named_Insts (map (fn (xi, p) => embed_indexname
-            ((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts);
-  in
-    (insts', fixes)
-  end;
+      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
@@ -120,32 +140,55 @@
 val inst =  Args.maybe Parse_Tools.name_term;
 val concl = Args.$$$ "concl" -- Args.colon;
 
-fun read_of_insts toks thm =
+fun close_unchecked_insts context ((insts,concl_inst), fixes) =
   let
-    val parser =
-      Parse.!!!
-        ((Scan.repeat (Scan.unless concl inst) -- Scan.optional (concl |-- Scan.repeat inst) [])
-          -- Parse.for_fixes) --| Scan.ahead Parse.eof;
-    val ((insts, concl_insts), fixes) =
-      the (Scan.read Token.stopper parser toks);
+    val ctxt = Context.proof_of context;
+    val ctxt1 = ctxt
+      |> Proof_Context.read_vars fixes |-> Proof_Context.add_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
+        #> Syntax.check_terms ctxt1
+        #> Variable.export_terms ctxt1 ctxt)
+      |> map (try the_single);
 
-    val insts' =
-      if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts)
-      then
-        Term_Insts
-          (map_filter
-            (Option.map (Parse_Tools.the_real_val #> unembed_indexname)) (insts @ concl_insts))
-      else
+    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, tok)) => embed_indexname ((xi, nm), tok))));
-  in
-    (insts', fixes)
-  end;
+          |> 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  =
+
+fun read_instantiate_closed ctxt (Named_Insts (insts, fixes)) thm  =
       let
         val insts' = map (fn ((v, t), _) => ((v, Position.none), t)) insts;
 
@@ -170,22 +213,42 @@
       in
         (thm'' |> restore_tags thm)
       end
-  | read_instantiate_closed _ ((Term_Insts insts), _) thm = instantiate_xis insts thm;
-
-val parse_all : Token.T list context_parser = Scan.lift (Scan.many Token.not_eof);
+  | 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 insts' thm end
+  | read_instantiate_closed _ (Term_Insts insts) thm = instantiate_xis insts thm;
 
 val _ =
   Theory.setup
-    (Attrib.setup @{binding "where"} (parse_all >>
-      (fn toks => Thm.rule_attribute (fn context =>
-        read_instantiate_closed (Context.proof_of context) (read_where_insts toks))))
+    (Attrib.setup @{binding "where"}
+      (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 Thm.rule_attribute (fn context =>
+            read_instantiate_closed (Context.proof_of context) args') end))
       "named instantiation of theorem");
 
 val _ =
   Theory.setup
-    (Attrib.setup @{binding "of"} (parse_all >>
-      (fn toks => Thm.rule_attribute (fn context => fn thm =>
-        read_instantiate_closed (Context.proof_of context) (read_of_insts toks thm) thm)))
+    (Attrib.setup @{binding "of"}
+      (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
+          Thm.rule_attribute (fn context => fn thm =>
+            if Method_Closure.is_free_thm thm andalso unchecked
+            then Method_Closure.dummy_free_thm
+            else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm)
+        end))
       "positional instantiation of theorem");
 
 end;
diff -r 014b86186c49 -r b4f1a0a701ae src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Sat May 16 12:05:52 2015 +0200
@@ -40,20 +40,20 @@
     Match_Term of term Item_Net.T
   | Match_Fact of thm Item_Net.T
   | Match_Concl
-  | Match_Prems;
+  | Match_Prems of bool;
 
 
 val aconv_net = Item_Net.init (op aconv) single;
 
 val parse_match_kind =
   Scan.lift @{keyword "conclusion"} >> K Match_Concl ||
-  Scan.lift @{keyword "premises"} >> K Match_Prems ||
+  Scan.lift (@{keyword "premises"} |-- Args.mode "local") >> Match_Prems ||
   Scan.lift (@{keyword "("}) |-- Args.term --| Scan.lift (@{keyword ")"}) >>
     (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 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_term : (term, binding) Parse_Tools.parse_val parser =
@@ -66,28 +66,24 @@
 
 val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
 
-fun pos_of dyn =
-  (case dyn of
-    Parse_Tools.Parse_Val (b, _) => Binding.pos_of b
-  | _ => raise Fail "Not a parse value");
-
+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. *)
 fun dynamic_fact ctxt =
   bound_term -- Args.opt_attribs (Attrib.check_name ctxt);
 
-type match_args = {multi : bool, cut : bool};
+type match_args = {multi : bool, cut : int};
 
 val parse_match_args =
   Scan.optional (Args.parens (Parse.enum1 ","
-    (Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
+    (Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.int 1))) [] >>
     (fn ss =>
       fold (fn s => fn {multi, cut} =>
         (case s of
-         "multi" => {multi = true, cut = cut}
-        | "cut" => {multi = multi, cut = true}))
-      ss {multi = false, cut = false});
+          ("multi", _) => {multi = true, cut = cut}
+        | ("cut", n) => {multi = multi, cut = n}))
+      ss {multi = false, cut = ~1});
 
 fun parse_named_pats match_kind =
   Args.context :|-- (fn ctxt =>
@@ -126,8 +122,22 @@
             then Syntax.parse_prop ctxt3 term
             else Syntax.parse_term ctxt3 term;
 
+          fun drop_Trueprop_dummy t =
+            (case t of
+              Const (@{const_name Trueprop}, _) $
+                (Const (@{syntax_const "_type_constraint_"}, T) $
+                  Const (@{const_name Pure.dummy_pattern}, _)) =>
+                    Const (@{syntax_const "_type_constraint_"}, T) $
+                      Const (@{const_name Pure.dummy_pattern}, propT)
+            | t1 $ t2 => drop_Trueprop_dummy t1 $ drop_Trueprop_dummy t2
+            | Abs (a, T, b) => Abs (a, T, drop_Trueprop_dummy b)
+            | _ => t);
+
           val pats =
             map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
+            |> map drop_Trueprop_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;
@@ -138,7 +148,7 @@
                 error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
               fix_nms fixes;
 
-          val _ = map (Term.map_types Type.no_tvars) pats
+          val _ = map (Term.map_types Type.no_tvars) pats;
 
           val ctxt4 = fold Variable.declare_term pats ctxt3;
 
@@ -200,14 +210,14 @@
                 |> 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 ((_, (Parse_Tools.Parse_Val (_, f), _)), t) => f t) (ts, pats');
+          val _ = ListPair.app (fn ((_, (v, _)), t) => Parse_Tools.the_parse_fun v t) (ts, pats');
 
           fun close_src src =
             let
               val src' = Token.closure_src src |> Token.transform_src morphism;
               val _ =
                 map2 (fn tok1 => fn tok2 =>
-                  (case (Token.get_value tok2) of
+                  (case Token.get_value tok2 of
                     SOME value => Token.assign (SOME value) tok1
                   | NONE => ()))
                   (Token.args_of_src src)
@@ -219,14 +229,14 @@
 
           val _ =
             ListPair.app
-              (fn ((SOME ((Parse_Tools.Parse_Val (_, f), _)), _), SOME (t, _)) => f t
+              (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 (( (Parse_Tools.Parse_Val (_, f), _) , _), t) => f t)
+            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;
@@ -255,7 +265,6 @@
   let
     val ts' = map (Envir.norm_term env) ts;
     val insts = map (Thm.cterm_of ctxt) ts' ~~ map (Thm.cterm_of ctxt) params;
-
   in
     Drule.cterm_instantiate insts thm
   end;
@@ -309,7 +318,6 @@
     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;
@@ -326,19 +334,28 @@
         tenv = tenv, tyenv = tyenv}
   end
 
-fun match_filter_env inner_ctxt morphism pat_vars fixes (ts, params) thm inner_env =
+fun morphism_env morphism env =
   let
-    val tenv = Envir.term_env inner_env
+    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;
 
-    val tyenv = Envir.type_env inner_env
-      |> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T)));
+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;
 
-    val outer_env = Envir.Envir {maxidx = Envir.maxidx_of inner_env, tenv = tenv, tyenv = tyenv};
-
+fun match_filter_env is_newly_fixed pat_vars fixes params env =
+  let
     val param_vars = map Term.dest_Var params;
 
-    val params' = map (fn (xi, _) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
+    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;
 
@@ -346,24 +363,21 @@
 
     val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
 
-    val tenv' = tenv
-      |> fold (Vartab.delete_safe) extra_vars;
+    val tenv' = tenv |> fold (Vartab.delete_safe) extra_vars;
 
     val env' =
-      Envir.Envir {maxidx = Envir.maxidx_of outer_env, tenv = tenv', tyenv = tyenv}
-      |> recalculate_maxidx;
+      Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env}
 
-    val all_params_bound = forall (fn SOME (_, Var _) => true | _ => false) params';
+    val all_params_bound = forall (fn SOME (_, Free (x,_)) => is_newly_fixed x | _ => false) params';
+
+    val all_params_distinct = not (has_duplicates (op =) 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;
-
-    val thm' = Morphism.thm morphism thm;
-
   in
-    if all_params_bound andalso all_pat_fixes_bound then
-      SOME (case ts of SOME ts => inst_thm inner_ctxt outer_env params ts thm' | _ => thm', env')
+    if all_params_bound andalso all_pat_fixes_bound andalso all_params_distinct
+    then SOME env'
     else NONE
   end;
 
@@ -374,7 +388,7 @@
 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);
+  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)
@@ -394,13 +408,34 @@
 
 val focus_prems = #1 o Focus_Data.get;
 
+fun hyp_from_premid ctxt (ident, prem) =
+  let
+    val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
+    val hyp =
+      (case #hyps (Thm.crep_thm prem) of
+        [hyp] => hyp
+      | _ => error "Prem should have exactly one hyp");  (* FIXME error vs. raise Fail !? *)
+    val ct = Drule.mk_term (hyp) |> Thm.cprop_of;
+  in Drule.protect (Conjunction.mk_conjunction (ident, ct)) end;
+
+fun hyp_from_ctermid ctxt (ident,cterm) =
+  let
+    val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term);
+  in Drule.protect (Conjunction.mk_conjunction (ident, cterm)) end;
+
+fun add_premid_hyp premid ctxt =
+  Thm.declare_hyps (hyp_from_premid ctxt premid) 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 thm =
+fun remove_focus_prem' (ident, thm) =
   (Focus_Data.map o @{apply 3(1)} o apsnd)
-    (Item_Net.remove (raw_thm_to_id thm, thm));
+    (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 _ =
@@ -429,22 +464,48 @@
   (Focus_Data.map o @{apply 3(3)})
     (append (map (fn (_, ct) => Thm.term_of ct) params));
 
+fun solve_term ct = Thm.trivial ct OF [Drule.termI];
+
+fun get_thinned_prems goal =
+  let
+    val chyps = Thm.crep_thm goal |> #hyps;
+
+    fun prem_from_hyp hyp goal =
+    let
+      val asm = Thm.assume hyp;
+      val (identt,ct) = asm |> Goal.conclude |> Thm.cprop_of |> Conjunction.dest_conjunction;
+      val ident = HOLogic.dest_number (Thm.term_of identt |> Logic.dest_term) |> snd;
+      val thm = Conjunction.intr (solve_term identt) (solve_term ct) |> Goal.protect 0
+      val goal' = Thm.implies_elim (Thm.implies_intr hyp goal) thm;
+    in
+      (SOME (ident,ct),goal')
+    end handle TERM _ => (NONE,goal) | THM _ => (NONE,goal);
+  in
+    fold_map prem_from_hyp chyps goal
+    |>> map_filter I
+  end;
+
 
 (* Add focus elements as proof data *)
-fun augment_focus
-    ({context, params, prems, asms, concl, schematics} : Subgoal.focus) : Subgoal.focus =
+fun augment_focus (focus: Subgoal.focus) : (int list * Subgoal.focus) =
   let
-    val context' = context
+    val {context, params, prems, asms, concl, schematics} = focus;
+
+    val (prem_ids,ctxt') = context
       |> add_focus_params params
       |> add_focus_schematics (snd schematics)
-      |> fold add_focus_prem (rev prems);
+      |> fold_map add_focus_prem (rev prems)
+
+    val local_prems = map2 pair prem_ids (rev prems);
+
+    val ctxt'' = fold add_premid_hyp local_prems ctxt';
   in
-    {context = context',
+    (prem_ids,{context = ctxt'',
      params = params,
      prems = prems,
      concl = concl,
      schematics = schematics,
-     asms = asms}
+     asms = asms})
   end;
 
 
@@ -467,25 +528,17 @@
       schematics = schematics', asms = asms} : Subgoal.focus, goal'')
   end;
 
-exception MATCH_CUT;
-
-val raise_match : (thm * Envir.env) Seq.seq = Seq.make (fn () => raise MATCH_CUT);
-
-fun map_handle seq =
-  Seq.make (fn () =>
-    (case (Seq.pull seq handle MATCH_CUT => NONE) of
-      SOME (x, seq') => SOME (x, map_handle seq')
-    | NONE => NONE));
 
 fun deduplicate eq prev seq =
   Seq.make (fn () =>
-    (case (Seq.pull seq) of
+    (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;
@@ -494,84 +547,135 @@
     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) =
-  let
-    val tyenv1 = Envir.type_env env1;
-    val tyenv2 = Envir.type_env env2;
-  in
     Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso
     ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) =>
-        (var = var' andalso
-          Envir.eta_contract (Envir.norm_term env1 t) aconv
-          Envir.eta_contract (Envir.norm_term env2 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 Envir.norm_type tyenv1 T = Envir.norm_type tyenv2 T')
-      (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2))
-  end;
+        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 is_cut (_, x : match_args) = #cut 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;
 
-    fun match_thm (((x, params), pat), thm) env  =
+    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 pat' = pat |> Envir.norm_term env;
-
-        val (((Tinsts', insts), [thm']), inner_ctxt) = Variable.import false [thm] ctxt;
-
-        val item' = Thm.prop_of thm';
-
         val ts = Option.map (fst o fst) (fst x);
 
-        val outer_ctxt = ctxt |> Variable.declare_maxidx (Envir.maxidx_of env);
-
-        val morphism = Variable.export_morphism inner_ctxt outer_ctxt;
+        val item' = Thm.prop_of thm;
 
         val matches =
-          (Unify.matchers (Context.Proof ctxt) [(pat', item')])
+          (Unify.matchers (Context.Proof ctxt) [(pat, item')])
           |> Seq.filter consistent_env
           |> Seq.map_filter (fn env' =>
-              match_filter_env inner_ctxt morphism pat_vars fixes
-                (ts, params) thm' (Envir.merge (env, 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_snd eq_env) []
-          |> is_cut x ? (fn t => Seq.make (fn () =>
-            Option.map (fn (x, _) => (x, raise_match)) (Seq.pull t)));
-      in
-        matches
-      end;
+          |> deduplicate (eq_pair Thm.eq_thm_prop eq_env) []
+      in matches end;
 
     val all_matches =
-      map (fn pat => (pat, get (snd pat))) prop_pats
+      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) =
-      if is_multi pat then
-        let
-          val empty = ([], Envir.empty ~1);
+      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 thmenvs' =
-            Seq.EVERY (map (fn e => fn (thms, env) =>
-              Seq.append (Seq.map (fn (thm, env') => (thm :: thms, env')) (e env))
-                (Seq.single (thms, env))) thmenvs) empty;
-        in
-          Seq.map_filter (fn (fact, env') =>
-            if not (null fact) then SOME ((pat, fact) :: pats, env') else NONE) thmenvs'
-        end
-      else
-        fold (fn e => Seq.append (Seq.map (fn (thm, env') =>
-          ((pat, [thm]) :: pats, env')) (e env))) thmenvs Seq.empty;
+            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.empty ~1)
+      Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1);
   in
-    map_handle all_matches
+    all_matches
+    |> Seq.map (apsnd (morphism_env morphism))
   end;
 
 fun real_match using ctxt fixes m text pats goal =
@@ -611,20 +715,24 @@
           let
             fun focus_cases f g =
               (case match_kind of
-                Match_Prems => f
+                Match_Prems b => f b
               | Match_Concl => g
               | _ => raise Fail "Match kind fell through");
 
-            val ({context = focus_ctxt, params, asms, concl, ...}, focused_goal) =
-              focus_cases (Subgoal.focus_prems) (focus_concl) ctxt 1 goal
+            val (goal_thins,goal) = get_thinned_prems goal;
+
+            val ((local_premids,{context = focus_ctxt, params, asms, concl, ...}), focused_goal) =
+              focus_cases (K Subgoal.focus_prems) (focus_concl) ctxt 1 goal
               |>> augment_focus;
 
             val texts =
               focus_cases
-                (fn _ =>
+                (fn is_local => fn _ =>
                   make_fact_matches focus_ctxt
-                    (Item_Net.retrieve (focus_prems focus_ctxt |> snd) #>
-                  order_list))
+                    (Item_Net.retrieve (focus_prems focus_ctxt |> snd)
+                     #> filter_out (member (eq_fst (op =)) goal_thins)
+                     #> 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)]))
                 ();
@@ -633,13 +741,34 @@
 
             fun do_retrofit inner_ctxt goal' =
               let
-                val cleared_prems =
-                  subtract (eq_fst (op =))
+                val (goal'_thins,goal') = get_thinned_prems goal';
+
+                val thinned_prems =
+                  ((subtract (eq_fst (op =))
                     (focus_prems inner_ctxt |> snd |> Item_Net.content)
-                    (focus_prems focus_ctxt |> snd |> Item_Net.content)
-                  |> map (fn (_, thm) =>
-                    Thm.hyps_of thm
-                    |> (fn [hyp] => hyp | _ => error "Prem should have only one hyp"));
+                    (focus_prems focus_ctxt |> snd |> Item_Net.content))
+                    |> map (fn (id, thm) =>
+                        #hyps (Thm.crep_thm thm)
+                        |> (fn [chyp] => (id, (SOME chyp, NONE))
+                             | _ => error "Prem should have only one hyp")));
+
+                val all_thinned_prems =
+                  thinned_prems @
+                  map (fn (id, prem) => (id, (NONE, SOME prem))) (goal'_thins @ goal_thins);
+
+                val (thinned_local_prems,thinned_extra_prems) =
+                  List.partition (fn (id, _) => member (op =) local_premids id) all_thinned_prems;
+
+                val local_thins =
+                  thinned_local_prems
+                  |> map (fn (_, (SOME t, _)) => Thm.term_of t
+                           | (_, (_, SOME pt)) => Thm.term_of pt |> Logic.dest_term);
+
+                val extra_thins =
+                  thinned_extra_prems
+                  |> map (fn (id, (SOME ct, _)) => (id, Drule.mk_term ct |> Thm.cprop_of)
+                           | (id, (_, SOME pt)) => (id, pt))
+                  |> map (hyp_from_ctermid inner_ctxt);
 
                 val n_subgoals = Thm.nprems_of goal';
                 fun prep_filter t =
@@ -648,12 +777,13 @@
                   if member (op =) prems t then SOME (remove1 (op aconv) t prems) else NONE;
               in
                 Subgoal.retrofit inner_ctxt ctxt params asms 1 goal' goal |>
-                (if n_subgoals = 0 orelse null cleared_prems then I
+                (if n_subgoals = 0 orelse null local_thins then I
                  else
                   Seq.map (Goal.restrict 1 n_subgoals)
                   #> Seq.maps (ALLGOALS (fn i =>
-                      DETERM (filter_prems_tac' ctxt prep_filter filter_test cleared_prems i)))
+                      DETERM (filter_prems_tac' ctxt prep_filter filter_test local_thins i)))
                   #> Seq.map (Goal.unrestrict 1))
+                  |> Seq.map (fold Thm.weaken extra_thins)
               end;
 
             fun apply_text (text, ctxt') =
@@ -661,7 +791,7 @@
                 val goal' =
                   DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal
                   |> Seq.maps (DETERM (do_retrofit ctxt'))
-                  |> Seq.map (fn goal => ([]: cases, goal))
+                  |> Seq.map (fn goal => ([]: cases, goal));
               in goal' end;
           in
             Seq.map apply_text texts
diff -r 014b86186c49 -r b4f1a0a701ae src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Sat May 16 12:05:52 2015 +0200
@@ -12,11 +12,15 @@
 sig
   val is_dummy: thm -> bool
   val tag_free_thm: thm -> thm
+  val is_free_thm: thm -> bool
+  val dummy_free_thm: thm
   val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute
-  val wrap_attribute: bool -> Binding.binding -> theory -> theory
+  val wrap_attribute: {handle_all_errs : bool, declaration : bool} ->
+    Binding.binding -> theory -> theory
   val read_inner_method: Proof.context -> Token.src -> Method.text
   val read_text_closure: Proof.context -> Token.src -> Token.src * Method.text
   val read_inner_text_closure: Proof.context -> Input.source -> Token.src * Method.text
+  val parse_method: Method.text context_parser
   val method_evaluate: Method.text -> Proof.context -> Method.method
   val get_inner_method: Proof.context -> string * Position.T ->
     (term list * (string list * string list)) * Method.text
@@ -87,11 +91,14 @@
     if exists is_free_thm (thm :: args) then dummy_free_thm
     else f context thm);
 
-fun free_aware_attribute thy declaration src (context, thm) =
+fun free_aware_attribute thy {handle_all_errs,declaration} src (context, thm) =
   let
     val src' = Token.init_assignable_src src;
     fun apply_att thm = (Attrib.attribute_global thy src') (context, thm);
-    val _ = try apply_att Drule.dummy_thm;
+    val _ =
+      if handle_all_errs then (try apply_att Drule.dummy_thm; ())
+      else (apply_att Drule.dummy_thm; ()) handle THM _ => () | TERM _ => () | TYPE _ => ();
+
     val src'' = Token.closure_src src';
     val thms =
       map_filter Token.get_value (Token.args_of_src src'')
@@ -104,13 +111,13 @@
     else apply_att thm
   end;
 
-fun wrap_attribute declaration binding thy =
+fun wrap_attribute args binding thy =
   let
     val name = Binding.name_of binding;
     val name' = Attrib.check_name_generic (Context.Theory thy) (name, Position.none);
     fun get_src src = Token.src (name', Token.range_of_src src) (Token.args_of_src src);
   in
-    Attrib.define_global binding (free_aware_attribute thy declaration o get_src) "" thy
+    Attrib.define_global binding (free_aware_attribute thy args o get_src) "" thy
     |> snd
   end;
 
@@ -133,8 +140,9 @@
     val method_text = read_inner_method ctxt src;
     val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
     (*FIXME: Does not markup method parameters. Needs to be done by Method.parser' directly. *)
-    val _ = Method.map_source (fn src =>
-                  (try (Method.check_name ctxt) (Token.name_of_src src);src)) method_text;
+    val _ =
+      Method.map_source (fn src => (try (Method.check_name ctxt) (Token.name_of_src src); src))
+        method_text;
     val src' = Token.closure_src src;
   in (src', method_text') end;
 
@@ -169,18 +177,18 @@
 fun parse_term_args args =
   Args.context :|-- (fn ctxt =>
     let
+      val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt;
+
       fun parse T =
-        (if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt)
+        (if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt')
         #> Type.constraint (Type_Infer.paramify_vars T);
 
       fun do_parse' T =
-        Parse_Tools.name_term >>
-          (fn Parse_Tools.Parse_Val (s, f) => (parse T s, f)
-            | Parse_Tools.Real_Val t' => (t', K ()));
+        Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T);
 
       fun do_parse (Var (_, T)) = do_parse' T
         | do_parse (Free (_, T)) = do_parse' T
-        | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt t);
+        | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t);
 
        fun rep [] x = Scan.succeed [] x
          | rep (t :: ts) x  = (do_parse t -- rep ts >> op ::) x;
@@ -188,7 +196,7 @@
       fun check ts =
         let
           val (ts, fs) = split_list ts;
-          val ts' = Syntax.check_terms ctxt ts |> Variable.polymorphic ctxt;
+          val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt';
           val _ = ListPair.app (fn (f, t) => f t) (fs, ts');
         in ts' end;
     in Scan.lift (rep args) >> check end);
@@ -218,7 +226,7 @@
   in Method.map_source (Token.transform_src morphism) text end;
 
 fun evaluate_dynamic_thm ctxt name =
-  (case (try (Named_Theorems.get ctxt) name) of
+  (case try (Named_Theorems.get ctxt) name of
     SOME thms => thms
   | NONE => Proof_Context.get_thms ctxt name);
 
@@ -247,6 +255,20 @@
 
 fun setup_local_fact binding = Named_Theorems.declare binding "";
 
+(* FIXME: In general we need the ability to override all dynamic facts.
+   This is also slow: we need Named_Theorems.only *)
+fun empty_named_thm named_thm ctxt =
+  let
+    val contents = Named_Theorems.get ctxt named_thm;
+    val attrib = snd oo Thm.proof_attributes [Named_Theorems.del named_thm];
+  in fold attrib contents ctxt end;
+
+fun dummy_named_thm named_thm ctxt =
+  let
+    val ctxt' = empty_named_thm named_thm ctxt;
+    val (_,ctxt'') = Thm.proof_attributes [Named_Theorems.add named_thm] dummy_free_thm ctxt';
+  in ctxt'' end;
+
 fun parse_method_args method_names =
   let
     fun bind_method (name, text) ctxt =
@@ -320,11 +342,13 @@
     fun parser args eval =
       apfst (Config.put_generic Method.old_section_parser true) #>
       (parse_term_args args --|
-        Method.sections modifiers --
-        (*Scan.depend (fn context => Scan.succeed () >> (K (fold XNamed_Theorems.empty uses_nms context, ()))) --*)  (* FIXME *)
-        parse_method_args method_names >> eval);
+        (Scan.depend (fn context =>
+              Scan.succeed (Context.map_proof (fold empty_named_thm uses_nms) context,())) --
+         Method.sections modifiers) --
+       parse_method_args method_names >> eval);
 
     val lthy3 = lthy2
+      |> fold dummy_named_thm named_thms
       |> Method.local_setup (Binding.make (Binding.name_of name, Position.none))
         (parser term_args
           (fn (fixes, decl) => fn ctxt => get_recursive_method ctxt fixes (decl ctxt))) "(internal)";
diff -r 014b86186c49 -r b4f1a0a701ae src/HOL/Eisbach/parse_tools.ML
--- a/src/HOL/Eisbach/parse_tools.ML	Wed May 13 19:12:59 2015 +0200
+++ b/src/HOL/Eisbach/parse_tools.ML	Sat May 16 12:05:52 2015 +0200
@@ -6,18 +6,21 @@
 
 signature PARSE_TOOLS =
 sig
+
   datatype ('a, 'b) parse_val =
     Real_Val of 'a
-  | Parse_Val of 'b * ('a -> unit)
+  | Parse_Val of 'b * ('a -> unit);
 
-  val parse_term_val : 'b parser -> (term, 'b) parse_val parser
-
-  val name_term : (term, string) parse_val parser
   val is_real_val : ('a, 'b) parse_val -> bool
 
   val the_real_val : ('a, 'b) parse_val -> 'a
   val the_parse_val : ('a, 'b) parse_val -> 'b
   val the_parse_fun : ('a, 'b) parse_val -> ('a -> unit)
+
+  val parse_val_cases: ('b -> 'a) -> ('a, 'b) parse_val -> ('a * ('a -> unit))
+
+  val parse_term_val : 'b parser -> (term, 'b) parse_val parser
+  val name_term : (term, string) parse_val parser
 end;
 
 structure Parse_Tools: PARSE_TOOLS =
@@ -46,4 +49,7 @@
 fun the_parse_fun (Parse_Val (_, f)) = f
   | the_parse_fun _ = raise Fail "Expected open parsed value";
 
+fun parse_val_cases g (Parse_Val (b, f)) = (g b, f)
+  | parse_val_cases _ (Real_Val v) = (v, K ());
+
 end;