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