updated Eisbach, using version 134bc592909c of its Bitbucket repository;

--- a/src/HOL/Eisbach/Tests.thy	Sun May 17 21:44:34 2015 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Sun May 17 22:33:34 2015 +0200
@@ -458,9 +458,36 @@
     done
 end
 
+subsection \<open>Proper context for method parameters\<close>
+
+method add_simp methods m uses f = (match f in H[simp]:_ \<Rightarrow> \<open>m\<close>)
+
+method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \<Rightarrow> \<open>m\<close>)
+
+method rule_my_thms = (rule my_thms_named)
+method rule_my_thms' declares my_thms_named = (rule my_thms_named)
+
+lemma
+  assumes A: A and B: B
+  shows
+  "(A \<or> B) \<and> A \<and> A \<and> A"
+  apply (intro conjI)
+  apply (add_simp \<open>add_simp \<open>simp\<close> f: B\<close> f: A)
+  apply (add_my_thms \<open>rule_my_thms\<close> f:A)
+  apply (add_my_thms \<open>rule_my_thms'\<close> f:A)
+  apply (add_my_thms \<open>rule my_thms_named\<close> f:A)
+  done
+
+subsection \<open>Shallow parser tests\<close>
+
+method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = (fail)
+
+lemma True
+  by (all_args True False \<open>-\<close> \<open>fail\<close> f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
 
 subsection \<open>Method name internalization test\<close>
 
+
 method test2 = (simp)
 
 method simp = fail

--- a/src/HOL/Eisbach/match_method.ML	Sun May 17 21:44:34 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Sun May 17 22:33:34 2015 +0200
@@ -60,9 +60,9 @@
   Parse_Tools.parse_term_val Parse.binding;
 
 val fixes =
-  Parse.and_list1 (Scan.repeat1  (Parse.position bound_term) --
+  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;
+    >> (fn (xs, T) => map (fn (x, pos) => ((x, T), pos)) xs)) >> flat;
 
 val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) [];
 
@@ -77,7 +77,7 @@
 
 val parse_match_args =
   Scan.optional (Args.parens (Parse.enum1 ","
-    (Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.int 1))) [] >>
+    (Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.nat 1))) [] >>
     (fn ss =>
       fold (fn s => fn {multi, cut} =>
         (case s of
@@ -87,14 +87,15 @@
 
 fun parse_named_pats match_kind =
   Args.context :|-- (fn ctxt =>
-    Scan.lift (Parse.and_list1 (Scan.option (dynamic_fact ctxt --| Args.colon) :--
-      (fn opt_dyn =>
-        if is_none opt_dyn orelse nameable_match match_kind
-        then Parse_Tools.name_term -- parse_match_args
-        else
-          let val b = #1 (the opt_dyn)
-          in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end))
-    -- for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.cartouche))
+    Scan.lift (Parse.and_list1
+      (Scan.option (dynamic_fact ctxt --| Args.colon) :--
+        (fn opt_dyn =>
+          if is_none opt_dyn orelse nameable_match match_kind
+          then Parse_Tools.name_term -- parse_match_args
+          else
+            let val b = #1 (the opt_dyn)
+            in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end))
+        -- for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.cartouche))
   >> (fn ((ts, fixes), cartouche) =>
     (case Token.get_value cartouche of
       SOME (Token.Source src) =>
@@ -249,10 +250,6 @@
         end)));
 
 
-fun parse_match_bodies match_kind =
-  Parse.enum1' "\<bar>" (parse_named_pats match_kind);
-
-
 fun dest_internal_fact t =
   (case try Logic.dest_conjunction t of
     SOME (params, head) =>
@@ -799,22 +796,19 @@
   end;
 
 val match_parser =
-  parse_match_kind :-- (fn kind => Scan.lift @{keyword "in"} |-- parse_match_bodies kind) >>
+  parse_match_kind :-- (fn kind =>
+      Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
     (fn (matches, bodies) => fn ctxt => fn using => fn goal =>
       if Method_Closure.is_dummy goal then Seq.empty
       else
         let
           fun exec (pats, fixes, text) goal =
             let
-              val ctxt' = fold Variable.declare_term fixes ctxt
-              |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*)
-            in
-              real_match using ctxt' fixes matches text pats goal
-            end;
-        in
-          Seq.FIRST (map exec bodies) goal
-          |> Seq.flat
-        end);
+              val ctxt' =
+                fold Variable.declare_term fixes ctxt
+                |> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*)
+            in real_match using ctxt' fixes matches text pats goal end;
+        in Seq.flat (Seq.FIRST (map exec bodies) goal) end);
 
 val _ =
   Theory.setup

--- a/src/HOL/Eisbach/method_closure.ML	Sun May 17 21:44:34 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Sun May 17 22:33:34 2015 +0200
@@ -25,7 +25,7 @@
   val get_inner_method: Proof.context -> string * Position.T ->
     (term list * (string list * string list)) * Method.text
   val eval_inner_method: Proof.context -> (term list * string list) * Method.text ->
-    term list -> (string * thm list) list -> Method.method list ->
+    term list -> (string * thm list) list -> (Proof.context -> Method.method) list ->
     Proof.context -> Method.method
   val method_definition: binding -> (binding * typ option * mixfix) list ->
     binding list -> binding list -> binding list -> Token.src -> local_theory -> local_theory
@@ -53,12 +53,12 @@
 structure Local_Data = Proof_Data
 (
   type T =
-    Method.method Symtab.table *  (*dynamic methods*)
+    (Proof.context -> Method.method) Symtab.table *  (*dynamic methods*)
     (term list -> Proof.context -> Method.method)  (*recursive method*);
   fun init _ : T = (Symtab.empty, fn _ => fn _ => Method.fail);
 );
 
-fun lookup_dynamic_method full_name ctxt =
+fun lookup_dynamic_method ctxt full_name =
   (case Symtab.lookup (#1 (Local_Data.get ctxt)) full_name of
     SOME m => m
   | NONE => error ("Illegal use of internal Eisbach method: " ^ quote full_name));
@@ -169,10 +169,6 @@
         error ("Unexpected inner token value for method cartouche" ^
           Position.here (Token.pos_of tok))));
 
-fun method_evaluate text ctxt : Method.method = fn facts => fn st =>
-  if is_dummy st then Seq.empty
-  else Method.evaluate text (Config.put Method.closure false ctxt) facts st;
-
 
 fun parse_term_args args =
   Args.context :|-- (fn ctxt =>
@@ -237,20 +233,28 @@
           Token.Fact (SOME name, evaluate_dynamic_thm ctxt name)
       | x => x);
 
+fun method_evaluate text ctxt : Method.method = fn facts => fn st =>
+  let
+    val ctxt' = Config.put Method.closure false ctxt;
+  in
+    if is_dummy st then Seq.empty
+    else Method.evaluate (evaluate_named_theorems ctxt' text) ctxt' facts st
+  end;
+
 fun evaluate_method_def fix_env raw_text ctxt =
   let
     val text = raw_text
-      |> instantiate_text fix_env
-      |> evaluate_named_theorems ctxt;
+      |> instantiate_text fix_env;
   in method_evaluate text ctxt end;
 
 fun setup_local_method binding lthy =
   let
     val full_name = Local_Theory.full_name lthy binding;
+    fun get_method ctxt = lookup_dynamic_method ctxt full_name ctxt;
   in
     lthy
-    |> update_dynamic_method (full_name, Method.fail)
-    |> Method.local_setup binding (Scan.succeed (lookup_dynamic_method full_name)) "(internal)"
+    |> update_dynamic_method (full_name, K Method.fail)
+    |> Method.local_setup binding (Scan.succeed get_method) "(internal)"
   end;
 
 fun setup_local_fact binding = Named_Theorems.declare binding "";
@@ -271,8 +275,11 @@
 
 fun parse_method_args method_names =
   let
-    fun bind_method (name, text) ctxt =
-      update_dynamic_method (name, method_evaluate text ctxt) ctxt;
+    fun bind_method (name, text) ctxt = 
+    let
+      val method = method_evaluate text;
+      val inner_update = method o update_dynamic_method (name,K (method ctxt));
+    in update_dynamic_method (name,inner_update) ctxt end;
 
     fun do_parse t = parse_method >> pair t;
     fun rep [] x = Scan.succeed [] x
@@ -341,11 +348,11 @@
 
     fun parser args eval =
       apfst (Config.put_generic Method.old_section_parser true) #>
-      (parse_term_args args --|
+      (parse_term_args args --
+        parse_method_args method_names --|
         (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);
+         Method.sections modifiers) >> eval);
 
     val lthy3 = lthy2
       |> fold dummy_named_thm named_thms
@@ -384,11 +391,11 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword method} "Eisbach method definition"
     (Parse.binding -- Parse.for_fixes --
-      ((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)) []) --
+      ((Scan.optional (@{keyword "methods"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
+        (Scan.optional (@{keyword "uses"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) [])) --
+      (Scan.optional (@{keyword "declares"} |-- Parse.!!! (Scan.repeat1 Parse.binding)) []) --
       Parse.!!! (@{keyword "="}
         |-- (Parse.position (Parse.args1 (K true)) >> (fn (args, pos) => Token.src ("", pos) args)))
-      >> (fn ((((name, vars), (uses, attribs)), methods), source) =>
+      >> (fn ((((name, vars), (methods, uses)), attribs), source) =>
         method_definition_cmd name vars uses attribs methods source));
 end;