# HG changeset patch
# User wenzelm
# Date 1703069704 -3600
# Node ID 7464bb64622da143e9e7b31b6cbfa785b46537e0
# Parent  140c7fac037aa43b4ac3ef8a9eebb8945c866064
clarified ML toplevel output: avoid "??." prefix;

diff -r 140c7fac037a -r 7464bb64622d src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Dec 20 11:16:39 2023 +0100
+++ b/src/Pure/Isar/proof_display.ML	Wed Dec 20 11:55:04 2023 +0100
@@ -46,12 +46,17 @@
   else Pretty.str "<context>");
 
 fun default_context mk_thy =
-  (case Context.get_generic_context () of
-    SOME (Context.Proof ctxt) => ctxt
-  | SOME (Context.Theory thy) =>
-      try Syntax.init_pretty_global thy
-      |> \<^if_none>\<open>Syntax.init_pretty_global (mk_thy ())\<close>
-  | NONE => Syntax.init_pretty_global (mk_thy ()));
+  let
+    fun global_context () =
+      Config.put_global Name_Space.names_long true (mk_thy ());
+  in
+    (case Context.get_generic_context () of
+      SOME (Context.Proof ctxt) => ctxt
+    | SOME (Context.Theory thy) =>
+        try Syntax.init_pretty_global thy
+        |> \<^if_none>\<open>Syntax.init_pretty_global (global_context ())\<close>
+    | NONE => Syntax.init_pretty_global (global_context ()))
+  end;
 
 fun pp_thm mk_thy th =
   Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;