--- a/src/Pure/Tools/profiling_report.scala Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/profiling_report.scala Tue Aug 29 12:53:28 2023 +0200
@@ -30,7 +30,7 @@
thy <- used_theories.iterator
if theories.isEmpty || theories.contains(thy)
snapshot <- Build.read_theory(session_context.theory(thy)).iterator
- (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
+ case (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
} yield if (clean_name) report.clean_name else report).toList
for (report <- ML_Profiling.account(reports)) progress.echo(report.print)