# HG changeset patch
# User wenzelm
# Date 950471652 -3600
# Node ID 36a85a6c4852aa95dad86bc2af96d1bf6fba7368
# Parent  85169951d515162caac1588c2e2260da5e84acb8
refine_end;

diff -r 85169951d515 -r 36a85a6c4852 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Feb 13 20:52:58 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Feb 13 20:54:12 2000 +0100
@@ -42,6 +42,7 @@
   type method
   val method: (thm list -> tactic) -> method
   val refine: (context -> method) -> state -> state Seq.seq
+  val refine_end: (context -> method) -> state -> state Seq.seq
   val find_free: term -> string -> term option
   val export_thm: context -> thm -> thm
   val match_bind: (string list * string) list -> state -> state
@@ -346,14 +347,16 @@
 
 (* refine goal *)
 
+local
+
 fun check_sign sg state =
   if Sign.subsig (sg, sign_of state) then state
   else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
 
-fun refine meth_fun state =
+fun gen_refine current_context meth_fun state =
   let
-    val Method meth = meth_fun (context_of state);
-    val (_, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
+    val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
+    val Method meth = meth_fun (if current_context then context_of state else goal_ctxt);
 
     fun refn thm' =
       state
@@ -361,6 +364,13 @@
       |> map_goal (K ((result, (facts, thm')), f));
   in Seq.map refn (meth facts thm) end;
 
+in
+
+val refine = gen_refine true;
+val refine_end = gen_refine false;
+
+end;
+
 
 (* export *)