src/Pure/Isar/proof.ML
changeset 24794 5740b01a1553
parent 24556 22ac3c8d78a5
child 24920 2a45e400fdad
     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') =>