# HG changeset patch
# User wenzelm
# Date 1695728044 -7200
# Node ID 1eca7abaa0159552cf45a670736e09fb7c3f978f
# Parent  97dfba4405e3c95ea8994e668796c05402594b6d
tuned;

diff -r 97dfba4405e3 -r 1eca7abaa015 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Sep 26 12:46:31 2023 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Sep 26 13:34:04 2023 +0200
@@ -783,10 +783,10 @@
               Command.print0 {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ =>
                 let
                   val _ = Output.status [Markup.markup_only Markup.consolidating];
-                  val res = Exn.capture (Thy_Info.apply_presentation context) thy;
+                  val result = Exn.capture (Thy_Info.apply_presentation context) thy;
                   val _ = Lazy.force (get_consolidated node);
                   val _ = Output.status [Markup.markup_only Markup.consolidated];
-                in Exn.release res end};
+                in Exn.release result end};
             val result_entry =
               (case lookup_entry node id of
                 NONE => err_undef "result command entry" id
diff -r 97dfba4405e3 -r 1eca7abaa015 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Sep 26 12:46:31 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Sep 26 13:34:04 2023 +0200
@@ -216,9 +216,9 @@
   | consolidate_theory (Exn.Res (Result {theory, exec_id, ...})) =
       let
         val _ = Execution.join [exec_id];
-        val res = Exn.capture Thm.consolidate_theory theory;
+        val result = Exn.capture Thm.consolidate_theory theory;
         val exns = maps Task_Queue.group_status (Execution.peek exec_id);
-      in res :: map Exn.Exn exns end;
+      in result :: map Exn.Exn exns end;
 
 fun present_theory (Exn.Exn exn) = [Exn.Exn exn]
   | present_theory (Exn.Res (Result {theory, present, ...})) =