diff -r 50c5b0912a0c -r 3702086a15a3 src/Pure/Tools/invoke.ML
--- 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;