src/Pure/thm_deps.ML

--- a/src/Pure/thm_deps.ML	Sat Jun 08 11:47:48 2024 +0200
+++ b/src/Pure/thm_deps.ML	Sat Jun 08 16:26:47 2024 +0200
@@ -73,17 +73,17 @@
 
 fun pretty_thm_deps thy thms =
   let
-    val ctxt = Proof_Context.init_global thy;
+    val facts = Global_Theory.facts_of thy;
+    val extern_fact = Name_Space.extern_generic (Context.Theory thy) (Facts.space_of facts);
     val deps =
       (case try (thm_deps thy) thms of
         SOME deps => deps
       | NONE => error "Malformed proofs");
     val items =
-      map #2 deps
-      |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i))
-      |> sort_by (#2 o #1)
-      |> map (fn ((marks, xname), i) =>
-          Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]);
+      deps
+      |> map (fn (_, thm_name as (name, _)) => (extern_fact name, thm_name))
+      |> sort_by #1
+      |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name thy thm_name])
   in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;