# HG changeset patch
# User wenzelm
# Date 1140202997 -3600
# Node ID 644a7a47ed0263460f9f24fcf7fbc693c0dbe855
# Parent  100bf66d7e85e8b58c9e54957f6852f0fa4a6db9
global_qeds: transfer body context;

diff -r 100bf66d7e85 -r 644a7a47ed02 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Feb 17 20:03:14 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Feb 17 20:03:17 2006 +0100
@@ -886,7 +886,7 @@
   #> Seq.map generic_qed
   #> Seq.maps (fn (((_, after_qed), results), state) =>
     Seq.lift after_qed results (theory_of state)
-    |> Seq.map (pair (context_of state)))
+    |> Seq.map (fn thy => (ProofContext.transfer thy (context_of state), thy)))
   |> Seq.DETERM;   (*backtracking may destroy theory!*)
 
 fun global_qed txt =