Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Tools/invoke.ML
changeset 19919 138e0684cda2
parent 19897 fe661eb3b0e7
child 20218 be3bfb0699ba 
--- 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)
isabelle