# HG changeset patch
# User wenzelm
# Date 1408459567 -7200
# Node ID 671c607fb4af5a384ecba7f49f9e08eed2a2b12e
# Parent  3072ff7ea4722eaab117c66113aee7443b306eec
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);

diff -r 3072ff7ea472 -r 671c607fb4af src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Aug 19 16:09:11 2014 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 19 16:46:07 2014 +0200
@@ -68,7 +68,7 @@
   val method: Proof.context -> src -> Proof.context -> method
   val method_closure: Proof.context -> src -> src
   val method_cmd: Proof.context -> src -> Proof.context -> method
-  val evaluate: text -> Proof.context -> Proof.context -> method
+  val evaluate: text -> 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
@@ -421,17 +421,17 @@
 
 in
 
-fun evaluate text static_ctxt =
+fun evaluate text ctxt =
   let
-    fun eval (Basic meth) = APPEND_CASES oo meth
-      | eval (Source src) = APPEND_CASES oo method_cmd static_ctxt src
+    fun eval (Basic meth) = APPEND_CASES o meth ctxt
+      | eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt
       | eval (Combinator (_, c, txts)) =
           let
             val comb = combinator c;
-            val meths = map eval txts
-          in fn ctxt => fn facts => comb (map (fn meth => meth ctxt facts) meths) end;
+            val meths = map eval txts;
+          in fn facts => comb (map (fn meth => meth facts) meths) end;
     val meth = eval text;
-  in fn ctxt => fn facts => fn st => meth ctxt facts ([], st) end;
+  in fn facts => fn st => meth facts ([], st) end;
 
 end;
 
diff -r 3072ff7ea472 -r 671c607fb4af src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Aug 19 16:09:11 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Aug 19 16:46:07 2014 +0200
@@ -395,10 +395,10 @@
   Rule_Cases.make_common
     (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
 
-fun apply_method meth state =
+fun apply_method text ctxt state =
   #2 (#2 (find_goal state))
   |> (fn {statement, messages = _, using, goal, before_qed, after_qed} =>
-    meth using goal
+    Method.evaluate text ctxt using goal
     |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
@@ -408,11 +408,8 @@
 
 in
 
-fun refine text state =
-  apply_method (Method.evaluate text (context_of state) (context_of state)) state;
-
-fun refine_end text state =
-  apply_method (Method.evaluate text (context_of state) (#1 (find_goal state))) state;
+fun refine text state = apply_method text (context_of state) state;
+fun refine_end text state = apply_method text (#1 (find_goal state)) state;
 
 fun refine_insert ths =
   Seq.hd o refine (Method.Basic (K (Method.insert ths)));