changeset 78592 | fdfe9b91d96e |
parent 75440 | 39011d0d2128 |
--- 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