tuned;

--- a/src/Pure/Isar/method.ML	Tue Aug 19 14:51:25 2014 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 19 15:10:37 2014 +0200
@@ -69,7 +69,7 @@
     local_theory -> local_theory
   val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     local_theory -> local_theory
-  val evaluate: Proof.context -> text -> Proof.context -> method
+  val evaluate: text -> Proof.context -> Proof.context -> method
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
@@ -413,7 +413,7 @@
 
 in
 
-fun evaluate static_ctxt text =
+fun evaluate text static_ctxt =
   let
     fun eval (Basic meth) = APPEND_CASES oo meth
       | eval (Source src) = APPEND_CASES oo method_cmd static_ctxt src

--- a/src/Pure/Isar/proof.ML	Tue Aug 19 14:51:25 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Aug 19 15:10:37 2014 +0200
@@ -395,26 +395,27 @@
   Rule_Cases.make_common
     (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
 
-fun apply_method current_context method state =
-  let
-    val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
-      find_goal state;
-    val ctxt = if current_context then context_of state else goal_ctxt;
-  in
-    method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
+fun apply_method meth state =
+  #2 (#2 (find_goal state))
+  |> (fn {statement, messages = _, using, goal, before_qed, after_qed} =>
+    meth using goal
+    |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
           (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
            Proof_Context.update_cases true meth_cases)
-          (K (statement, [], using, goal', before_qed, after_qed)) I)
-  end;
+          (K (statement, [], using, goal', before_qed, after_qed)) I));
 
 in
 
-fun refine text state = apply_method true (Method.evaluate (context_of state) text) state;
-fun refine_end text state = apply_method false (Method.evaluate (context_of state) text) state;
+fun refine text state =
+  apply_method (Method.evaluate text (context_of state) (context_of state)) state;
 
-fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_end text state =
+  apply_method (Method.evaluate text (context_of state) (#1 (find_goal state))) state;
+
+fun refine_insert ths =
+  Seq.hd o refine (Method.Basic (K (Method.insert ths)));
 
 end;