tuned;

--- a/src/Pure/Admin/build_fonts.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -284,7 +284,7 @@
       val domain =
         (for ((name, index) <- targets if index == 0)
           yield Fontforge.font_domain(target_dir + hinted_path(false) + name))
-        .flatten.toSet.toList.sorted
+        .flatten.distinct.sorted
 
       Fontforge.execute(
         Fontforge.commands(

--- a/src/Pure/Admin/build_jdk.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -144,7 +144,7 @@
         val extracted = archives.map(extract_archive(dir, _))
 
         val version =
-          extracted.map(_._1).toSet.toList match {
+          extracted.map(_._1).distinct match {
             case List(version) => version
             case Nil => error("No archives")
             case versions =>

--- a/src/Pure/Admin/jenkins.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Admin/jenkins.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -106,7 +106,7 @@
         Isabelle_System.mkdirs(log_dir)
 
         val ml_statistics =
-          session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
+          session_logs.map(_._1).distinct.sorted.flatMap(session_name =>
             read_ml_statistics(store, session_name).
               map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
 

--- a/src/Pure/Thy/sessions.scala	Fri Mar 27 22:01:27 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 27 22:06:35 2020 +0100
@@ -271,7 +271,7 @@
                   if !ok(path.canonical_file)
                   path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
                 } yield (path1, name)).toList
-              val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).toSet.toList.sorted
+              val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
 
               val errs1 =
                 for { (path1, name) <- bad }