proper data_domain for symmetric difference;

--- a/src/Pure/Tools/build_process.scala	Sat Jul 08 15:52:57 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sat Jul 08 16:07:45 2023 +0200
@@ -288,7 +288,7 @@
       old_data: Map[String, A]
     ): Map[String, A] = {
       val dom = data_domain -- old_data.keysIterator
-      val data = old_data -- old_data.keysIterator.filterNot(dom)
+      val data = old_data -- old_data.keysIterator.filterNot(data_domain)
       if (dom.isEmpty) data
       else data_iterator(dom).foldLeft(data) { case (map, a) => map + (a.name -> a) }
     }