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 =