# HG changeset patch
# User wenzelm
# Date 1719831558 -7200
# Node ID 3490a9c96d2f9232d148a16020f5c992e81ff8db
# Parent  7a1f9e57104655d71c0057ec6f8615090d0f2474
tuned;

diff -r 7a1f9e571046 -r 3490a9c96d2f src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Mon Jul 01 12:40:54 2024 +0200
+++ b/src/Pure/Build/build_job.scala	Mon Jul 01 12:59:18 2024 +0200
@@ -229,7 +229,7 @@
                   try {
                     val (rc, errs) = {
                       import XML.Decode._
-                      pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
+                      pair(int, list(self))(Symbol.decode_yxml(msg.text))
                     }
                     val errors =
                       for (err <- errs) yield {
diff -r 7a1f9e571046 -r 3490a9c96d2f src/Pure/Build/export_theory.scala
--- a/src/Pure/Build/export_theory.scala	Mon Jul 01 12:40:54 2024 +0200
+++ b/src/Pure/Build/export_theory.scala	Mon Jul 01 12:59:18 2024 +0200
@@ -395,7 +395,7 @@
       val (typargs, (args, (prop_body, proof_body))) = {
         import XML.Decode._
         import Term_XML.Decode._
-        pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body)
+        pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(self, self)))(body)
       }
       val env = args.toMap
       val prop = Term_XML.Decode.term_env(env)(prop_body)
diff -r 7a1f9e571046 -r 3490a9c96d2f src/Pure/General/graph_display.scala
--- a/src/Pure/General/graph_display.scala	Mon Jul 01 12:40:54 2024 +0200
+++ b/src/Pure/General/graph_display.scala	Mon Jul 01 12:59:18 2024 +0200
@@ -54,7 +54,7 @@
     build_graph(
       {
         import XML.Decode._
-        list(pair(pair(string, pair(string, x => x)), list(string)))(body)
+        list(pair(pair(string, pair(string, self)), list(string)))(body)
       })
 
   def make_graph[A](