changeset 72683 | b5e6f0d137a7 |
parent 72682 | e0443773ef1a |
child 72691 | 2126cf946086 |
--- a/src/Pure/Thy/export.scala Sat Nov 21 20:35:48 2020 +0100 +++ b/src/Pure/Thy/export.scala Sat Nov 21 21:02:38 2020 +0100 @@ -244,7 +244,7 @@ context: Sessions.Database_Context, session: String, theory_name: String): Provider = new Provider { def apply(export_name: String): Option[Entry] = - context.try_export(session, theory_name, export_name) + context.read_export(session, theory_name, export_name) def focus(other_theory: String): Provider = this