# HG changeset patch
# User wenzelm
# Date 1526753955 -7200
# Node ID 3c1a716e7f599e75f42de608430bb953adb3a13d
# Parent  dbef88c2b6c59645885682a064ce82093ea4f909
tuned queries;

diff -r dbef88c2b6c5 -r 3c1a716e7f59 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat May 19 20:05:13 2018 +0200
+++ b/src/Pure/Thy/export.scala	Sat May 19 20:19:15 2018 +0200
@@ -46,7 +46,15 @@
       stmt.execute_query().iterator(res => res.string(Data.name)).toList)
   }
 
-  def read_theory_names(db: SQL.Database, session_name: String): List[(String, String)] =
+  def read_theory_names(db: SQL.Database, session_name: String): List[String] =
+  {
+    val select =
+      Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)
+    db.using_statement(select)(stmt =>
+      stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
+  }
+
+  def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] =
   {
     val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
     db.using_statement(select)(stmt =>
@@ -255,7 +263,7 @@
     using(store.open_database(session_name))(db =>
     {
       db.transaction {
-        val export_names = read_theory_names(db, session_name)
+        val export_names = read_theory_exports(db, session_name)
 
         // list
         if (export_list) {
diff -r dbef88c2b6c5 -r 3c1a716e7f59 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat May 19 20:05:13 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sat May 19 20:19:15 2018 +0200
@@ -32,9 +32,8 @@
       using(store.open_database(session_name))(db =>
       {
         db.transaction {
-          Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator.
-            map((theory_name: String) =>
-              read_theory(db, session_name, theory_name, types = types, consts = consts)).toList
+          Export.read_theory_names(db, session_name).map((theory_name: String) =>
+            read_theory(db, session_name, theory_name, types = types, consts = consts))
         }
       })