src/Pure/Tools/profiling_report.scala
changeset 78592 fdfe9b91d96e
parent 78280 865b44cbaad1
--- 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)