# HG changeset patch
# User wenzelm
# Date 1430406177 -7200
# Node ID 022ca2799c731f69451c8b0699cc2b358a5ae23d
# Parent  d72795f401c35284f8b413ac2646311e3f8e1399
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;

diff -r d72795f401c3 -r 022ca2799c73 src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy	Thu Apr 30 17:02:57 2015 +0200
@@ -8,14 +8,15 @@
 imports Pure
 keywords
   "method" :: thy_decl and
-  "concl"
-  "prems"  (* FIXME conflict with "prems" in Isar, which is presently dormant *)
+  "conclusion"
+  "premises"
   "declares"
   "methods"
   "\<bar>" "\<Rightarrow>"
   "uses"
 begin
 
+
 ML_file "parse_tools.ML"
 ML_file "eisbach_rule_insts.ML"
 ML_file "method_closure.ML"
@@ -38,6 +39,6 @@
     Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
   "rotated theorem premises"
 
-method solves methods m = \<open>m; fail\<close>
+method solves methods m = (m; fail)
 
 end
diff -r d72795f401c3 -r 022ca2799c73 src/HOL/Eisbach/Eisbach_Tools.thy
--- a/src/HOL/Eisbach/Eisbach_Tools.thy	Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy	Thu Apr 30 17:02:57 2015 +0200
@@ -35,7 +35,12 @@
       (Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
       (fn ctxt => fn (tok, t) =>
         (* FIXME proper formatting!? *)
-        Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t));
+        Token.unparse tok ^ ": " ^ Syntax.string_of_term ctxt t) #>
+    setup_trace_method @{binding print_type}
+      (Scan.lift (Scan.ahead Parse.not_eof) -- Args.typ)
+      (fn ctxt => fn (tok, t) =>
+        (* FIXME proper formatting!? *)
+        Token.unparse tok ^ ": " ^ Syntax.string_of_typ ctxt t));
 
 end
 \<close>
diff -r d72795f401c3 -r 022ca2799c73 src/HOL/Eisbach/Examples.thy
--- a/src/HOL/Eisbach/Examples.thy	Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Examples.thy	Thu Apr 30 17:02:57 2015 +0200
@@ -11,19 +11,19 @@
 
 subsection \<open>Basic methods\<close>
 
-method my_intros = \<open>rule conjI | rule impI\<close>
+method my_intros = (rule conjI | rule impI)
 
 lemma "P \<and> Q \<longrightarrow> Z \<and> X"
   apply my_intros+
   oops
 
-method my_intros' uses intros = \<open>rule conjI | rule impI | rule intros\<close>
+method my_intros' uses intros = (rule conjI | rule impI | rule intros)
 
 lemma "P \<and> Q \<longrightarrow> Z \<or> X"
   apply (my_intros' intros: disjI1)+
   oops
 
-method my_spec for x :: 'a = \<open>drule spec[where x="x"]\<close>
+method my_spec for x :: 'a = (drule spec[where x="x"])
 
 lemma "\<forall>x. P x \<Longrightarrow> P x"
   apply (my_spec x)
@@ -34,11 +34,11 @@
 subsection \<open>Focusing and matching\<close>
 
 method match_test =
-  \<open>match prems in U: "P x \<and> Q x" for P Q x \<Rightarrow>
+  (match premises in U: "P x \<and> Q x" for P Q x \<Rightarrow>
     \<open>print_term P,
      print_term Q,
      print_term x,
-     print_fact U\<close>\<close>
+     print_fact U\<close>)
 
 lemma "\<And>x. P x \<and> Q x \<Longrightarrow> A x \<and> B x \<Longrightarrow> R x y \<Longrightarrow> True"
   apply match_test  -- \<open>Valid match, but not quite what we were expecting..\<close>
@@ -51,8 +51,6 @@
   back
   back
   back
-  back
-  back
   oops
 
 text \<open>Use matching to avoid "improper" methods\<close>
@@ -60,18 +58,18 @@
 lemma focus_test:
   shows "\<And>x. \<forall>x. P x \<Longrightarrow> P x"
   apply (my_spec "x :: 'a", assumption)?  -- \<open>Wrong x\<close>
-  apply (match concl in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
+  apply (match conclusion in "P x" for x \<Rightarrow> \<open>my_spec x, assumption\<close>)
   done
 
 
 text \<open>Matches are exclusive. Backtracking will not occur past a match\<close>
 
 method match_test' =
-  \<open>match concl in
+  (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>
-  \<close>
+  )
 
 text \<open>Solves goal\<close>
 lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q"
@@ -89,20 +87,20 @@
 
 
 method my_spec_guess =
-  \<open>match concl in "P (x :: 'a)" for P x \<Rightarrow>
+  (match conclusion in "P (x :: 'a)" for P x \<Rightarrow>
     \<open>drule spec[where x=x],
      print_term P,
-     print_term x\<close>\<close>
+     print_term x\<close>)
 
 lemma "\<forall>x. P (x :: nat) \<Longrightarrow> Q (x :: nat)"
   apply my_spec_guess
   oops
 
 method my_spec_guess2 =
-  \<open>match prems in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
+  (match premises in U[thin]:"\<forall>x. P x \<longrightarrow> Q x" and U':"P x" for P Q x \<Rightarrow>
     \<open>insert spec[where x=x, OF U],
      print_term P,
-     print_term Q\<close>\<close>
+     print_term Q\<close>)
 
 lemma "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> Q x \<Longrightarrow> Q x"
   apply my_spec_guess2?  -- \<open>Fails. Note that both "P"s must match\<close>
@@ -118,7 +116,7 @@
 subsection \<open>Higher-order methods\<close>
 
 method higher_order_example for x methods meth =
-  \<open>cases x, meth, meth\<close>
+  (cases x, meth, meth)
 
 lemma
   assumes A: "x = Some a"
@@ -129,12 +127,12 @@
 subsection \<open>Recursion\<close>
 
 method recursion_example for x :: bool =
-  \<open>print_term x,
+  (print_term x,
      match (x) in "A \<and> B" for A B \<Rightarrow>
-    \<open>(print_term A,
+    \<open>print_term A,
      print_term B,
      recursion_example A,
-     recursion_example B) | -\<close>\<close>
+     recursion_example B | -\<close>)
 
 lemma "P"
   apply (recursion_example "(A \<and> D) \<and> (B \<and> C)")
@@ -151,15 +149,15 @@
 
 subsection \<open>Demo\<close>
 
-method solve methods m = \<open>m;fail\<close>
+method solve methods m = (m; fail)
 
 named_theorems intros and elims and subst
 
 method prop_solver declares intros elims subst =
-  \<open>(assumption |
+  (assumption |
     rule intros | erule elims |
     subst subst | subst (asm) subst |
-    (erule notE; solve \<open>prop_solver\<close>))+\<close>
+    (erule notE; solve \<open>prop_solver\<close>))+
 
 lemmas [intros] =
   conjI
@@ -177,11 +175,11 @@
   done
 
 method guess_all =
-  \<open>match prems in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
-    \<open>match prems in "?H (y :: 'a)" for y \<Rightarrow>
+  (match premises in U[thin]:"\<forall>x. P (x :: 'a)" for P \<Rightarrow>
+    \<open>match premises in "?H (y :: 'a)" for y \<Rightarrow>
        \<open>rule allE[where P = P and x = y, OF U]\<close>
-   | match concl in "?H (y :: 'a)" for y \<Rightarrow>
-       \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>\<close>
+   | match conclusion in "?H (y :: 'a)" for y \<Rightarrow>
+       \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
 
 lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P y \<Longrightarrow> Q y"
   apply guess_all
@@ -193,10 +191,10 @@
   done
 
 method guess_ex =
-  \<open>match concl in
+  (match conclusion in
     "\<exists>x. P (x :: 'a)" for P \<Rightarrow>
-      \<open>match prems in "?H (x :: 'a)" for x \<Rightarrow>
-              \<open>rule exI[where x=x]\<close>\<close>\<close>
+      \<open>match premises in "?H (x :: 'a)" for x \<Rightarrow>
+              \<open>rule exI[where x=x]\<close>\<close>)
 
 lemma "P x \<Longrightarrow> \<exists>x. P x"
   apply guess_ex
@@ -204,7 +202,7 @@
   done
 
 method fol_solver =
-  \<open>(guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>\<close>
+  ((guess_ex | guess_all | prop_solver) ; solve \<open>fol_solver\<close>)
 
 declare
   allI [intros]
diff -r d72795f401c3 -r 022ca2799c73 src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy	Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Thu Apr 30 17:02:57 2015 +0200
@@ -8,12 +8,12 @@
 imports Main Eisbach_Tools
 begin
 
+
 section \<open>Named Theorems Tests\<close>
 
 named_theorems foo
 
-method foo declares foo =
-  \<open>rule foo\<close>
+method foo declares foo = (rule foo)
 
 lemma
   assumes A [foo]: A
@@ -30,12 +30,12 @@
 
   fix A y
   have "(\<And>x. A x) \<Longrightarrow> A y"
-    apply (rule dup, match prems 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 prems 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 prems in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match concl in "P y" for y \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=y]\<close>\<close>)
-    apply (rule dup, match prems in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match concl in "P z" for z \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=z]\<close>\<close>)
-    apply (rule dup, match concl in "P y" for P \<Rightarrow> \<open>match prems in Y: "\<And>z. P z" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
-    apply (match prems in Y: "\<And>z :: 'a. P z" for P \<Rightarrow> \<open>match concl in "P y" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
+    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"
@@ -44,37 +44,48 @@
     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 prems 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 prems in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
-    apply (match prems in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
-    apply (match concl in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
+    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 prems in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match prems in Y': "\<And>z :: 'b. B z" \<Rightarrow> \<open>print_fact Y, print_fact Y', rule Y'[where z=x]\<close>\<close>)
+    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 prems in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>)
-    apply (match prems in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match prems in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>fastforce\<close>\<close>)
-    apply (match prems in Y[thin]: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>(match prems in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>fail\<close> \<bar> Y': "?H" \<Rightarrow> \<open>-\<close>)\<close>)
+    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 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 prems in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
+    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 prems in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
+    apply (match premises in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
     apply (insert TrueI)
-    apply (match prems in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
+    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
 
@@ -82,33 +93,33 @@
   (* 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 prems in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
-    apply (match prems in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
-    apply (match prems in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
+    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> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* 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 prems in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
-    apply (match prems in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
-    apply (match prems in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
+    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> \<open>fail\<close> \<bar> "C y" \<Rightarrow> \<open>-\<close>) (* multi-match must bind something *)
+    apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
     done
 
 
   (*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 prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
-    apply (match prems 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 prems in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
-    apply (match prems in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
+    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>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
 
   (* 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 prems 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 prems 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 (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
 
@@ -123,20 +134,31 @@
   (* 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 prems 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>)
+    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
 
   have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
-    by (((match prems in I: "P \<and> Q" (cut)
+    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 "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
-    by (((match prems in I: "P \<and> Q" (cut)
+    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> \<open>fail\<close>\<close>
+        | simp add: X)
+
 end
 
 (* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
@@ -144,7 +166,7 @@
    legitimate pairs.*)
 
 schematic_lemma "?A x \<Longrightarrow> A x"
-  apply (match concl in "H" for H \<Rightarrow> \<open>match concl in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
+  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
 
@@ -171,7 +193,7 @@
       NONE => ()
     | SOME _ => error "Found internal fact")\<close>
 
-method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = \<open>rule uses_test\<^sub>1_uses\<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)
 
@@ -184,9 +206,9 @@
 (* Testing term and fact passing in recursion *)
 
 method recursion_example for x :: bool uses facts =
-  \<open>match (x) in
+  (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>\<close>
+  \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>)
 
 lemma
   assumes asms: "A" "B" "C" "D"
@@ -196,11 +218,11 @@
   done
 
 (*Method.sections in existing method*)
-method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = \<open>simp add: my_simp\<^sub>1_facts\<close>
+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 = \<open>uses_test\<^sub>1 uses_test\<^sub>1_uses: uses_test\<^sub>2_uses\<close>
+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)
 
 
@@ -208,7 +230,7 @@
 
 named_theorems declare_facts\<^sub>1
 
-method declares_test\<^sub>1 declares declare_facts\<^sub>1 = \<open>rule declare_facts\<^sub>1\<close>
+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)
 
@@ -218,28 +240,58 @@
 subsection \<open>Rule Instantiation Tests\<close>
 
 method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" =
-  \<open>erule allE [where x = x and P = P]\<close>
+  (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" =
-  \<open>erule allE [of P x]\<close>
+  (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" =
-  \<open>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>\<close>
+  (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" =
-  \<open>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>\<close>
+  (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)
 
 
+
+(* Polymorphism test *)
+
+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"
+
+lemmas my_thms = foo'_ax1 foo'_ax2
+
+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
+
+
 ML {*
 structure Data = Generic_Data
 (
@@ -254,7 +306,7 @@
 
 setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close>
 
-method dynamic_thms_test = \<open>rule test_dyn\<close>
+method dynamic_thms_test = (rule test_dyn)
 
 locale foo =
   fixes A
@@ -269,4 +321,12 @@
 
 end
 
+(* Method name internalization test *)
+
+method test2 = (simp)
+
+method simp = fail
+
+lemma "A \<Longrightarrow> A" by test2
+
 end
diff -r d72795f401c3 -r 022ca2799c73 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Thu Apr 30 17:02:57 2015 +0200
@@ -46,8 +46,8 @@
 val aconv_net = Item_Net.init (op aconv) single;
 
 val parse_match_kind =
-  Scan.lift @{keyword "concl"} >> K Match_Concl ||
-  Scan.lift @{keyword "prems"} >> K Match_Prems ||
+  Scan.lift @{keyword "conclusion"} >> K Match_Concl ||
+  Scan.lift @{keyword "premises"} >> K 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));
@@ -60,8 +60,8 @@
   Parse_Tools.parse_term_val Parse.binding;
 
 val fixes =
-  Parse.and_list1 (Scan.repeat1 bound_term --
-    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (rpair T) xs))
+  Parse.and_list1 (Scan.repeat1  (Parse.position bound_term) --
+    Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (fn (nm,pos) => ((nm,T),pos)) xs))
   >> flat;
 
 val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
@@ -77,18 +77,17 @@
 fun dynamic_fact ctxt =
   bound_term -- Args.opt_attribs (Attrib.check_name ctxt);
 
-type match_args = {unify : bool, multi : bool, cut : bool};
+type match_args = {multi : bool, cut : bool};
 
 val parse_match_args =
   Scan.optional (Args.parens (Parse.enum1 ","
-    (Args.$$$ "unify" || Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
+    (Args.$$$ "multi" || Args.$$$ "cut"))) [] >>
     (fn ss =>
-      fold (fn s => fn {unify, multi, cut} =>
+      fold (fn s => fn {multi, cut} =>
         (case s of
-          "unify" => {unify = true, multi = multi, cut = cut}
-        | "multi" => {unify = unify, multi = true, cut = cut}
-        | "cut" => {unify = unify, multi = multi, cut = true}))
-      ss {unify = false, multi = false, cut = false});
+         "multi" => {multi = true, cut = cut}
+        | "cut" => {multi = multi, cut = true}))
+      ss {multi = false, cut = false});
 
 (*TODO: Shape holes in thms *)
 fun parse_named_pats match_kind =
@@ -114,12 +113,12 @@
                   (Parse_Tools.the_real_val b,
                     map (Attrib.attribute ctxt) att)) b, match_args), v)
                 | _ => raise Fail "Expected closed term") ts
-          val fixes' = map (fn (p, _) => Parse_Tools.the_real_val p) fixes
+          val fixes' = map (fn ((p, _),_) => Parse_Tools.the_real_val p) fixes
         in (ts', fixes', text) end
     | SOME _ => error "Unexpected token value in match cartouche"
     | NONE =>
         let
-          val fixes' = map (fn (pb, otyp) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
+          val fixes' = map (fn ((pb, otyp),_) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
           val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt;
           val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
 
@@ -134,6 +133,14 @@
             map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
             |> 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_nms fixes;
+
+          val _ = map (Term.map_types Type.no_tvars) pats
+
           val ctxt4 = fold Variable.declare_term pats ctxt3;
 
           val (Ts, ctxt5) = ctxt4 |> fold_map Proof_Context.inferred_param fix_nms;
@@ -146,12 +153,6 @@
             | reject_extra_free _ () = ();
           val _ = (fold o fold_aterms) reject_extra_free pats ();
 
-          (*fun test_multi_bind {multi = multi, ...} pat = multi andalso
-           not (null (inter (op =) (map Free (Term.add_frees pat [])) real_fixes)) andalso
-           error "Cannot fix terms in multi-match. Use a schematic instead."
-
-          val _ = map2 (fn pat => fn (_, (_, match_args)) => test_multi_bind match_args pat) pats ts*)
-
           val binds =
             map (fn (b, _) => Option.map (fn (b, att) => (Parse_Tools.the_parse_val b, att)) b) ts;
 
@@ -184,7 +185,7 @@
             |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
             ||> Proof_Context.restore_mode ctxt;
 
-          val (src, text) = Method_Closure.read_text_closure ctxt6 (Token.input_of cartouche);
+          val (src, text) = Method_Closure.read_inner_text_closure ctxt6 (Token.input_of cartouche);
 
           val morphism =
             Variable.export_morphism ctxt6
@@ -206,7 +207,7 @@
 
           val real_fixes' = map (Morphism.term morphism) real_fixes;
           val _ =
-            ListPair.app (fn ((Parse_Tools.Parse_Val (_, f), _), t) => f t) (fixes, real_fixes');
+            ListPair.app (fn (( (Parse_Tools.Parse_Val (_, f),_) , _), t) => f t) (fixes, real_fixes');
 
           val match_args = map (fn (_, (_, match_args)) => match_args) ts;
           val binds'' = (binds' ~~ match_args) ~~ pats';
@@ -234,19 +235,9 @@
   let
     val ts' = map (Envir.norm_term env) ts;
     val insts = map (Thm.cterm_of ctxt) ts' ~~ map (Thm.cterm_of ctxt) params;
-    val tags = Thm.get_tags thm;
 
-   (*
-    val Tinsts = Type.raw_matches ((map (fastype_of) params), (map (fastype_of) ts')) Vartab.empty
-    |> Vartab.dest
-    |> map (fn (xi, (S, typ)) => (certT (TVar (xi, S)), certT typ))
-   *)
-
-    val thm' = Drule.cterm_instantiate insts thm
-    (*|> Thm.instantiate (Tinsts, [])*)
-      |> Thm.map_tags (K tags);
   in
-    thm'
+    Drule.cterm_instantiate insts thm
   end;
 
 fun do_inst fact_insts' env text ctxt =
@@ -282,6 +273,7 @@
 
     val morphism =
       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);
 
     val text' = Method.map_source (Token.transform_src morphism) text;
@@ -303,32 +295,61 @@
     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 match_filter_env ctxt fixes (ts, params) thm env =
+fun recalculate_maxidx env =
   let
+    val tenv = Envir.term_env env;
+    val tyenv = Envir.type_env env;
+    val max_tidx = Vartab.fold (fn (_,(_,t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
+    val max_Tidx = Vartab.fold (fn (_,(_,T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
+  in
+    Envir.Envir
+      {maxidx = Int.max (Int.max (max_tidx,max_Tidx),Envir.maxidx_of env),
+        tenv = tenv, tyenv = tyenv}
+  end
+
+fun match_filter_env inner_ctxt morphism pat_vars fixes (ts, params) thm inner_env =
+  let
+    val tenv = Envir.term_env inner_env
+      |> Vartab.map (K (fn (T,t) => (Morphism.typ morphism T,Morphism.term morphism t)));
+
+    val tyenv = Envir.type_env inner_env
+      |> Vartab.map (K (fn (S,T) => (S,Morphism.typ morphism T)));
+
+    val outer_env = Envir.Envir {maxidx = Envir.maxidx_of inner_env, tenv = tenv, tyenv = tyenv};
+
     val param_vars = map Term.dest_Var params;
-    val params' = map (Envir.lookup env) param_vars;
+
+    val params' = map (fn (xi,_) => Vartab.lookup (Envir.term_env outer_env) xi) param_vars;
 
     val fixes_vars = map Term.dest_Var fixes;
 
-    val tenv = Envir.term_env env;
     val all_vars = Vartab.keys tenv;
 
     val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars;
 
-    val tenv' = Envir.term_env env
+    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};
+      Envir.Envir {maxidx = Envir.maxidx_of outer_env, tenv = tenv', tyenv = tyenv}
+      |> recalculate_maxidx;
+
+    val all_params_bound = forall (fn SOME (_,(Var _)) => true | _ => false) params';
+
+    val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars;
 
-    val all_params_bound = forall (fn SOME (Var _) => true | _ => false) params';
+    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
-    then SOME (case ts of SOME ts => inst_thm ctxt env params ts thm | _ => thm, env')
+    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')
     else NONE
   end;
 
@@ -436,28 +457,78 @@
 
 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
+      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 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')))
+      (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;
+
+
 fun match_facts ctxt fixes prop_pats get =
   let
     fun is_multi (((_, x : match_args), _), _) = #multi x;
-    fun is_unify (_, x : match_args) = #unify x;
     fun is_cut (_, x : match_args) = #cut x;
 
     fun match_thm (((x, params), pat), thm) env  =
       let
         fun try_dest_term term = the_default term (try Logic.dest_term term);
 
+        val pat_vars = Term.add_vars pat [];
+
         val pat' = pat |> Envir.norm_term env |> try_dest_term;
 
-        val item' = Thm.prop_of thm |> try_dest_term;
+        val (((Tinsts', insts),[thm']), inner_ctxt) = Variable.import false [thm] ctxt
+
+        val item' = Thm.prop_of thm' |> try_dest_term;
+
         val ts = Option.map (fst o fst) (fst x);
-        (*FIXME: Do we need to move one of these patterns above the other?*)
+
+        val outer_ctxt = ctxt |> Variable.declare_maxidx (Envir.maxidx_of env);
+
+        val morphism = Variable.export_morphism inner_ctxt outer_ctxt;
 
         val matches =
-          (if is_unify x
-           then Unify.smash_unifiers (Context.Proof ctxt) [(pat', item') ] env
-           else 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 ctxt fixes (ts, params) thm (Envir.merge (env, env')))
+              match_filter_env inner_ctxt morphism pat_vars fixes
+                (ts, params) thm' (Envir.merge (env, env')))
+          |> 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
@@ -487,12 +558,6 @@
 
     val all_matches =
       Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1)
-      |> Seq.filter (fn (_, e) => forall (is_some o Envir.lookup e o Term.dest_Var) fixes);
-
-    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));
   in
     map_handle all_matches
   end;
diff -r d72795f401c3 -r 022ca2799c73 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Thu Apr 30 17:00:50 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Thu Apr 30 17:02:57 2015 +0200
@@ -14,7 +14,8 @@
   val tag_free_thm: thm -> thm
   val free_aware_rule_attribute: thm list -> (Context.generic -> thm -> thm) -> Thm.attribute
   val read_inner_method: Proof.context -> Token.src -> Method.text
-  val read_text_closure: Proof.context -> Input.source -> 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 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
@@ -22,9 +23,9 @@
     term list -> (string * thm list) list -> Method.method list ->
     Proof.context -> Method.method
   val method_definition: binding -> (binding * typ option * mixfix) list ->
-    binding list -> binding list -> binding list -> Input.source -> local_theory -> local_theory
+    binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
   val method_definition_cmd: binding -> (binding * string option * mixfix) list ->
-    binding list -> binding list -> binding list -> Input.source -> local_theory -> local_theory
+    binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
 end;
 
 structure Method_Closure: METHOD_CLOSURE =
@@ -97,38 +98,36 @@
     val parser = Parse.!!! (Method.parser' ctxt 0 --| Scan.ahead Parse.eof);
   in
     (case Scan.read Token.stopper parser toks of
-      SOME (method_text, _) => method_text
+      SOME (method_text, pos) => (Method.report (method_text, pos); method_text)
     | NONE => error ("Failed to parse method" ^ Position.here (#2 (Token.name_of_src src))))
   end;
 
-fun read_text_closure ctxt input =
+fun read_text_closure ctxt source =
   let
-    (*tokens*)
+    val src = Token.init_assignable_src source;
+    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 src' = Token.closure_src src;
+  in (src', method_text') end;
+
+fun read_inner_text_closure ctxt input =
+  let
     val keywords = Thy_Header.get_keywords' ctxt;
     val toks =
       Input.source_explode input
       |> Token.read_no_commands keywords (Scan.one Token.not_eof);
-    val _ =
-      toks |> List.app (fn tok =>
-        if Token.keyword_with Symbol.is_ascii_identifier tok then
-          Context_Position.report ctxt (Token.pos_of tok) Markup.keyword1
-        else ());
+  in read_text_closure ctxt (Token.src ("", Input.pos_of input) toks) end;
 
-    (*source closure*)
-    val src =
-      Token.src ("", Input.pos_of input) toks
-      |> Token.init_assignable_src;
-    val method_text = read_inner_method ctxt src;
-    val method_text' = Method.map_source (Method.method_closure ctxt) method_text;
-    val src' = Token.closure_src src;
-  in (src', method_text') end;
 
 val parse_method =
   Args.context -- Scan.lift (Parse.token Parse.cartouche) >> (fn (ctxt, tok) =>
     (case Token.get_value tok of
       NONE =>
         let
-           val (src, text) = read_text_closure ctxt (Token.input_of tok);
+           val input = Token.input_of tok;
+           val (src,text) = read_inner_text_closure ctxt input;
            val _ = Token.assign (SOME (Token.Source src)) tok;
         in text end
     | SOME (Token.Source src) => read_inner_method ctxt src
@@ -274,7 +273,7 @@
     fn ctxt => evaluate_method_def (match fixes) text (setup_ctxt ctxt)
   end;
 
-fun gen_method_definition prep_vars name vars uses attribs methods body lthy =
+fun gen_method_definition prep_vars name vars uses attribs methods source lthy =
   let
     val (uses_nms, lthy1) = lthy
       |> Proof_Context.concealed
@@ -304,7 +303,7 @@
         (parser term_args
           (fn (fixes, decl) => fn ctxt => get_recursive_method ctxt fixes (decl ctxt))) "(internal)";
 
-    val (src, text) = read_text_closure lthy3 body;
+    val (src, text) = read_text_closure lthy3 source;
 
     val morphism =
       Variable.export_morphism lthy3
@@ -338,7 +337,8 @@
       ((Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
         (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) --
       (Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
-      Parse.!!! (@{keyword "="} |-- Parse.token Parse.cartouche)
-      >> (fn ((((name, vars), (uses, attribs)), methods), cartouche) =>
-        method_definition_cmd name vars uses attribs methods (Token.input_of cartouche)));
+      Parse.!!! (@{keyword "="}
+        |-- (Parse.position (Parse.args1 (K true)) >> (fn (args, pos) => Token.src ("", pos) args)))
+      >> (fn ((((name, vars), (uses, attribs)), methods), source) =>
+        method_definition_cmd name vars uses attribs methods source));
 end;