# HG changeset patch
# User wenzelm
# Date 1748790563 -7200
# Node ID b77163d7e8478f28076b25805ffd12ceb82dc581
# Parent  f7f8bb1c28cede7bf08bf7baf59dd35ae2860b53
tuned;

diff -r f7f8bb1c28ce -r b77163d7e847 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jun 01 17:06:33 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 01 17:09:23 2025 +0200
@@ -166,8 +166,7 @@
 
 fun get_theory_elements name =
   let
-    val theory = get_theory name;
-    val keywords = Thy_Header.get_keywords theory;
+    val keywords = Thy_Header.get_keywords (get_theory name);
     val stopper = Document_Output.segment_stopper;
     val segments = get_theory_segments name;
   in Thy_Element.parse_elements_generic keywords #span stopper segments end;
@@ -207,7 +206,7 @@
     val _ = List.app (ignore o get thys') parents;
   in new_entry name parents (SOME deps, SOME res) thys' end;
 
-fun update_thy deps res = change_thys (update deps res);
+val update_thy = change_thys oo update;
 
 
 (* scheduling loader tasks *)