--- a/NEWS Sun May 04 12:18:27 2025 +0100
+++ b/NEWS Sun May 04 15:05:51 2025 +0200
@@ -59,6 +59,12 @@
not available as SVG.
+*** Pure ***
+
+* Command 'thy_deps' expects optional theory arguments as long theory names,
+the same way as the 'imports' clause. Minor INCOMPATIBILITY.
+
+
*** HOL ***
* Normalization by evaluation (method "normalization", command value) could
--- a/src/Pure/Tools/thy_deps.ML Sun May 04 12:18:27 2025 +0100
+++ b/src/Pure/Tools/thy_deps.ML Sun May 04 15:05:51 2025 +0200
@@ -36,6 +36,6 @@
let val thy0 = Proof_Context.theory_of ctxt
in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
-val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps (Theory.check {long = false});
+val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps (Theory.check {long = true});
end;