changeset 23351 | 3702086a15a3 |
parent 22769 | 6f5068e26b89 |
child 24493 | d4380e9b287b |
--- a/src/Pure/Tools/invoke.ML Wed Jun 13 00:01:41 2007 +0200 +++ b/src/Pure/Tools/invoke.ML Wed Jun 13 00:01:51 2007 +0200 @@ -93,7 +93,8 @@ "invoke" NONE after_qed propp |> Element.refine_witness |> Seq.hd - |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))))) + |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))), + Position.none)) |> Seq.hd end;