diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala Tue Aug 29 12:04:13 2023 +0200 +++ b/src/Pure/Tools/simplifier_trace.scala Tue Aug 29 12:53:28 2023 +0200 @@ -208,7 +208,7 @@ def purge(queue: Vector[Long]): Unit = queue match { case s +: rest => - for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s)) + for (case Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s)) memory -= Index.of_data(data) val children = memory_children.getOrElse(s, Set.empty) memory_children -= s