author | wenzelm |
Sat, 17 Jun 2006 19:38:01 +0200 | |
changeset 19919 | 138e0684cda2 |
parent 19918 | 5be127990076 |
child 19920 | 8257e52164a1 |
--- 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)