# HG changeset patch
# User haftmann
# Date 1746363951 -7200
# Node ID 766a07ff7a07a497cb7ae044de80625b0c247c51
# Parent  328de89f20f9e54a17dc3f2f6c958ad91d76bb62
consolidate input syntax

diff -r 328de89f20f9 -r 766a07ff7a07 NEWS
--- 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
diff -r 328de89f20f9 -r 766a07ff7a07 src/Pure/Tools/thy_deps.ML
--- 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;