apply current morphism to method text before evaluating;

--- a/src/HOL/Eisbach/Tests.thy	Mon May 30 20:58:54 2016 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Mon May 30 16:11:53 2016 +1000
@@ -262,9 +262,21 @@
 ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1_uses"\<close>
 ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close>
 
+subsection \<open>Basic fact passing\<close>
+
+method find_fact for x y :: bool uses facts1 facts2 =
+  (match facts1 in U: "x" \<Rightarrow> \<open>insert U,
+      match facts2 in U: "y" \<Rightarrow> \<open>insert U\<close>\<close>)
+
+lemma assumes A: A and B: B shows "A \<and> B"
+  apply (find_fact "A" "B" facts1: A facts2: B)
+  apply (rule conjI; assumption)
+  done
+
 
 subsection \<open>Testing term and fact passing in recursion\<close>
 
+
 method recursion_example for x :: bool uses facts =
   (match (x) in
     "A \<and> B" for A B \<Rightarrow> \<open>(recursion_example A facts: facts, recursion_example B facts: facts)\<close>
@@ -530,4 +542,53 @@
   apply (test_method' a b rule: assms [symmetric])?
   done
 
+subsection \<open>Eisbach methods in locales\<close>
+
+locale my_locale1 = fixes A assumes A: A begin
+
+method apply_A =
+  (match conclusion in "A" \<Rightarrow>
+    \<open>match A in U:"A" \<Rightarrow>
+      \<open>print_term A, print_fact A, rule U\<close>\<close>)
+
 end
+
+locale my_locale2 = fixes B assumes B: B begin
+
+interpretation my_locale1 B by (unfold_locales; rule B)
+
+lemma B by apply_A
+
+end
+
+context fixes C assumes C: C begin
+
+interpretation my_locale1 C by (unfold_locales; rule C)
+
+lemma C by apply_A
+
+end
+
+context begin
+
+interpretation my_locale1 "True \<longrightarrow> True" by (unfold_locales; blast)
+
+lemma "True \<longrightarrow> True" by apply_A
+
+end
+
+locale locale_poly = fixes P assumes P: "\<And>x :: 'a. P x" begin
+
+method solve_P for z :: 'a = (rule P[where x = z]) 
+
+end
+
+context begin
+
+interpretation locale_poly "\<lambda>x:: nat. 0 \<le> x" by (unfold_locales; blast)
+
+lemma "0 \<le> (n :: nat)" by (solve_P n)
+
+end
+
+end

--- a/src/HOL/Eisbach/match_method.ML	Mon May 30 20:58:54 2016 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Mon May 30 16:11:53 2016 +1000
@@ -54,6 +54,9 @@
 fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems _ => true | _ => false);
 fun prop_match m = (case m of Match_Term _ => false | _ => true);
 
+val bound_thm : (thm, binding) Parse_Tools.parse_val parser =
+  Parse_Tools.parse_thm_val Parse.binding;
+
 val bound_term : (term, binding) Parse_Tools.parse_val parser =
   Parse_Tools.parse_term_val Parse.binding;
 
@@ -69,7 +72,7 @@
 (*FIXME: Dynamic facts modify the background theory, so we have to resort
   to token replacement for matched facts. *)
 val dynamic_fact =
-  Scan.lift bound_term -- Attrib.opt_attribs;
+  Scan.lift bound_thm -- Attrib.opt_attribs;
 
 type match_args = {multi : bool, cut : int};
 
@@ -190,7 +193,7 @@
                     |> snd
                     |> Variable.declare_maxidx (Thm.maxidx_of head_thm);
                 in
-                  (SOME (Thm.prop_of head_thm, att) :: tms, ctxt''')
+                  (SOME (head_thm, att) :: tms, ctxt''')
                 end
             | upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt);
 
@@ -221,7 +224,7 @@
             in src' end;
 
           val binds' =
-            map (Option.map (fn (t, atts) => (Morphism.term morphism t, map close_src atts))) binds;
+            map (Option.map (fn (t, atts) => (Morphism.thm morphism t, map close_src atts))) binds;
 
           val _ =
             ListPair.app
@@ -245,13 +248,14 @@
         end));
 
 
-fun dest_internal_fact t =
+fun dest_internal_term t =
   (case try Logic.dest_conjunction t of
     SOME (params, head) =>
      (params |> Logic.dest_conjunctions |> map Logic.dest_term,
       head |> Logic.dest_term)
   | NONE => ([], t |> Logic.dest_term));
 
+fun dest_internal_fact thm = dest_internal_term (Thm.prop_of thm);
 
 fun inst_thm ctxt env ts params thm =
   let
@@ -266,7 +270,7 @@
         (fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att))
           | _ => NONE) fact_insts';
 
-    fun try_dest_term thm = try (Thm.prop_of #> dest_internal_fact #> snd) thm;
+    fun try_dest_term thm = try (dest_internal_fact #> snd) thm;
 
     fun expand_fact fact_insts thm =
       the_default [thm]

--- a/src/HOL/Eisbach/method_closure.ML	Mon May 30 20:58:54 2016 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Mon May 30 16:11:53 2016 +1000
@@ -260,14 +260,18 @@
 
     val text' = (Method.map_source o map) (Token.transform morphism) text;
     val term_args' = map (Morphism.term morphism) term_args;
+    val full_name = Local_Theory.full_name lthy name;
   in
     lthy3
     |> Local_Theory.close_target
     |> Proof_Context.restore_naming lthy
     |> put_closure name
         {vars = term_args', named_thms = named_thms, methods = method_args, body = text'}
-    |> Method.local_setup name (parser term_args' (recursive_method term_args' text')) ""
-    |> pair (Local_Theory.full_name lthy name)
+    |> Method.local_setup name 
+        (Args.context :|-- (fn ctxt =>
+          let val {body, vars, ...} = get_closure ctxt full_name in
+            parser vars (recursive_method vars body) end)) ""
+    |> pair full_name
   end;
 
 in

--- a/src/HOL/Eisbach/parse_tools.ML	Mon May 30 20:58:54 2016 +0200
+++ b/src/HOL/Eisbach/parse_tools.ML	Mon May 30 16:11:53 2016 +1000
@@ -20,6 +20,8 @@
 
   val parse_term_val : 'b parser -> (term, 'b) parse_val parser
   val name_term : (term, string) parse_val parser
+
+  val parse_thm_val : 'b parser -> (thm, 'b) parse_val parser
 end;
 
 structure Parse_Tools: PARSE_TOOLS =
@@ -36,6 +38,11 @@
 
 val name_term = parse_term_val Args.embedded_inner_syntax;
 
+fun parse_thm_val scan =
+  Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option (Args.internal_fact >> the_single)) -- scan >>
+    (fn ((_, SOME t), _) => Real_Val t
+      | ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Fact (NONE, [t]))) tok)));
+
 fun is_real_val (Real_Val _) = true
   | is_real_val _ = false;