# HG changeset patch
# User wenzelm
# Date 1191244496 -7200
# Node ID 5740b01a155354dfc709f4db3734987077d3fab1
# Parent  cbe63f2193b606726addc9d547ba043263a6771b
ContextPosition.put_ctxt;

diff -r cbe63f2193b6 -r 5740b01a1553 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Oct 01 15:14:55 2007 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Oct 01 15:14:56 2007 +0200
@@ -389,7 +389,8 @@
   let
     val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
       find_goal state;
-    val ctxt = ContextPosition.put pos (if current_context then context_of state else goal_ctxt);
+    val ctxt = ContextPosition.put_ctxt pos
+      (if current_context then context_of state else goal_ctxt);
     val meth = meth_fun ctxt;
   in
     Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>