src/Pure/Tools/invoke.ML

       [(("", []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
        (("", []), map (rpair [] o Logic.mk_term) params'),
        (("", []), 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';
 
           val types'' = map (Logic.dest_type o Thm.term_of o Drule.dest_term) res_types;

           ctxt
           |> ProofContext.sticky_prefix prfx
           |> 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
       "invoke" NONE after_qed propp
     |> Element.refine_witness