ContextPosition.put_ctxt;
authorwenzelm
Mon Oct 01 15:14:56 2007 +0200 (2007-10-01)
changeset 247945740b01a1553
parent 24793 cbe63f2193b6
child 24795 6f5cb7885fd7
ContextPosition.put_ctxt;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Oct 01 15:14:55 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Oct 01 15:14:56 2007 +0200
     1.3 @@ -389,7 +389,8 @@
     1.4    let
     1.5      val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
     1.6        find_goal state;
     1.7 -    val ctxt = ContextPosition.put pos (if current_context then context_of state else goal_ctxt);
     1.8 +    val ctxt = ContextPosition.put_ctxt pos
     1.9 +      (if current_context then context_of state else goal_ctxt);
    1.10      val meth = meth_fun ctxt;
    1.11    in
    1.12      Method.apply meth using goal |> Seq.map (fn (meth_cases, goal') =>