discontinued somewhat pointless dependency: avoid illusion of extra accuracy (see also 09fb749d1a1e and 0f750a6dc754);

--- a/src/Pure/ML_Bootstrap.thy	Sat Dec 17 19:09:46 2022 +0100
+++ b/src/Pure/ML_Bootstrap.thy	Sat Dec 17 19:19:10 2022 +0100
@@ -8,8 +8,6 @@
 imports Pure
 begin
 
-external_file "$POLYML_EXE"
-
 ML \<open>
   #allStruct ML_Name_Space.global () |> List.app (fn (name, _) =>
     if member (op =) ML_Name_Space.hidden_structures name then

--- a/src/Pure/Tools/build.scala	Sat Dec 17 19:09:46 2022 +0100
+++ b/src/Pure/Tools/build.scala	Sat Dec 17 19:19:10 2022 +0100
@@ -249,13 +249,11 @@
           (_, base) <- build_deps.session_bases.iterator
           (path, _) <- base.session_sources.iterator
         } yield path).toList
-      val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
-      val unknown_files =
-        Mercurial.check_files(source_files)._2.
-          filterNot(path => exclude_files.contains(path.canonical_file))
-      if (unknown_files.nonEmpty) {
-        progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
-          unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
+      Mercurial.check_files(source_files)._2 match {
+        case Nil =>
+        case unknown_files =>
+          progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
+            unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
       }
     }