# HG changeset patch
# User wenzelm
# Date 1262615753 -3600
# Node ID e18b0f7b9902f6e547ebf24432146b87a28e0c88
# Parent  b28be884eddad46c816d1484e537422ab4a70ff8
after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;

diff -r b28be884edda -r e18b0f7b9902 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jan 04 11:55:23 2010 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Jan 04 15:35:53 2010 +0100
@@ -862,14 +862,10 @@
     val results =
       tl (conclude_goal goal_ctxt goal stmt)
       |> burrow (ProofContext.export goal_ctxt outer_ctxt);
-
-    val (after_local, after_global) = after_qed;
-    fun after_local' x y = Position.setmp_thread_data pos (fn () => after_local x y) ();
-    fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
   in
     outer_state
     |> map_context (after_ctxt props)
-    |> pair ((after_local', after_global'), results)
+    |> pair (after_qed, results)
   end;
 
 end;