tuned;
authorwenzelm
Sun, 01 Jun 2025 17:09:23 +0200
changeset 82681 b77163d7e847
parent 82680 f7f8bb1c28ce
child 82682 06aac7eaec29
tuned;
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 *)