diff -r 500a3373c93c -r 16c8f44b1852 src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Wed Aug 02 22:26:58 2006 +0200
+++ b/src/Pure/Tools/invoke.ML	Wed Aug 02 22:26:59 2006 +0200
@@ -60,7 +60,7 @@
        (("", []), map (rpair [] o Element.mark_witness) prems')];
     fun after_qed results =
       Proof.end_block #>
-      Seq.map (Proof.map_context (fn ctxt =>
+      Proof.map_context (fn ctxt =>
         let
           val ([res_types, res_params, res_prems], ctxt'') =
             fold_burrow (apfst snd oo Variable.import false) results ctxt';
@@ -82,7 +82,8 @@
           |> ProofContext.qualified_names
           |> (snd o ProofContext.note_thmss_i notes)
           |> ProofContext.restore_naming ctxt
-        end) #> Proof.put_facts NONE);
+        end) #>
+      Proof.put_facts NONE #> Seq.single;
   in
     state'
     |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i