src/Pure/Tools/profiling_report.scala
changeset 78280 865b44cbaad1
parent 78178 a177f71dc79f
child 78592 fdfe9b91d96e
--- a/src/Pure/Tools/profiling_report.scala	Sun Jul 09 17:39:46 2023 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Sun Jul 09 17:41:02 2023 +0200
@@ -29,7 +29,7 @@
             (for {
               thy <- used_theories.iterator
               if theories.isEmpty || theories.contains(thy)
-              snapshot <- Build_Job.read_theory(session_context.theory(thy)).iterator
+              snapshot <- Build.read_theory(session_context.theory(thy)).iterator
               (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
             } yield if (clean_name) report.clean_name else report).toList