ProofContext.exports: simultaneous facts;
authorwenzelm
Sat, 17 Jun 2006 19:38:01 +0200
changeset 19919 138e0684cda2
parent 19918 5be127990076
child 19920 8257e52164a1
ProofContext.exports: simultaneous facts;
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)