# HG changeset patch
# User paulson
# Date 1746388984 -3600
# Node ID 43f4f9c5c6bdd2fcd6a3335ffebf77a87062d1e3
# Parent  98571d7e4a7dee41512f2a54f4fb7f896bda1b72# Parent  f62666eea755bccd6bc17ff839f8671fab56e6b5
merged

diff -r f62666eea755 -r 43f4f9c5c6bd NEWS
--- a/NEWS	Sun May 04 21:02:54 2025 +0100
+++ b/NEWS	Sun May 04 21:03:04 2025 +0100
@@ -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 f62666eea755 -r 43f4f9c5c6bd src/HOL/List.thy
--- a/src/HOL/List.thy	Sun May 04 21:02:54 2025 +0100
+++ b/src/HOL/List.thy	Sun May 04 21:03:04 2025 +0100
@@ -2440,6 +2440,19 @@
 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
   by (simp add: set_conv_nth) force
 
+lemma set_list_update:
+  "set (xs [i := k]) = insert k (set (take i xs) \<union> set (drop (Suc i) xs))"
+  if \<open>i < length xs\<close>
+using that proof (induct xs arbitrary: i)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons x xs i)
+  then show ?case
+    by (cases i) (simp_all add: insert_commute)
+qed
+
 
 subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
 
diff -r f62666eea755 -r 43f4f9c5c6bd src/Pure/Tools/thy_deps.ML
--- a/src/Pure/Tools/thy_deps.ML	Sun May 04 21:02:54 2025 +0100
+++ b/src/Pure/Tools/thy_deps.ML	Sun May 04 21:03:04 2025 +0100
@@ -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;