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