simplified Proof.end_block;

--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 02 22:26:58 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 02 22:26:59 2006 +0200
@@ -506,7 +506,7 @@
 val endP =
   OuterSyntax.command "}" "end explicit proof block"
     (K.tag_proof K.prf_close)
-    (Scan.succeed (Toplevel.print o Toplevel.proofs Proof.end_block));
+    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
 
 val nextP =
   OuterSyntax.command "next" "enter next proof block"

--- 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