diff -r ce44e714d573 -r 27a8e9e8761e src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Tue Dec 27 11:44:37 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Tue Dec 27 12:00:37 2022 +0100
@@ -153,9 +153,7 @@
     }
 
     private def make_entries[A](batches: List[List[Entry[A]]]): List[Entry[A]] = {
-      val item_batches =
-        batches.map(_.flatMap(
-          { case item: Item[_] => Some(item.asInstanceOf[Item[A]]) case _ => None }))
+      val item_batches = batches.map(_.flatMap(Library.as_subclass(classOf[Item[A]])))
       val sep_entries: List[Entry[A]] =
         item_batches.filter(_.nonEmpty).zipWithIndex.flatMap({ case (batch, i) =>
           Separator[A](i) :: batch.map(_.copy(batch = i))