ContextPosition.put_ctxt;

--- 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') =>