# HG changeset patch
# User wenzelm
# Date 1150565881 -7200
# Node ID 138e0684cda272a256c55d46d9cb24832568f3dc
# Parent  5be127990076ec82813e07c2c469ccbcb9f34c2e
ProofContext.exports: simultaneous facts;

diff -r 5be127990076 -r 138e0684cda2 src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Sat Jun 17 19:38:00 2006 +0200
+++ b/src/Pure/Tools/invoke.ML	Sat Jun 17 19:38:01 2006 +0200
@@ -74,7 +74,7 @@
           val Element.Notes notes = 
             Element.Notes (maps (Element.facts_of thy) elems')
             |> Element.satisfy_ctxt prems''
-            |> Element.map_ctxt_values I I (ProofContext.export ctxt'' ctxt);
+            |> Element.map_ctxt_values I I (singleton (ProofContext.export ctxt'' ctxt));
             (* FIXME export typs/terms *)
           val notes' = notes
             |> Attrib.map_facts (Attrib.attribute_i thy)