# HG changeset patch
# User wenzelm
# Date 1725621558 -7200
# Node ID 7d8b1ed1f74844766d951584100a138205c64e46
# Parent  1f718be3608b44ffdb843ebb7af095d2fb311144
tuned;

diff -r 1f718be3608b -r 7d8b1ed1f748 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu Sep 05 21:16:53 2024 +0200
+++ b/src/Pure/Isar/proof_display.ML	Fri Sep 06 13:19:18 2024 +0200
@@ -49,14 +49,17 @@
 fun guess_context () =
   let
     fun global_context () =
-      Config.put_global Name_Space.names_long true (Theory.get_pure ());
+      Theory.get_pure ()
+      |> Config.put_global Name_Space.names_long true
+      |> Syntax.init_pretty_global;
   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 ()))
+        (case try Syntax.init_pretty_global thy of
+          SOME ctxt => ctxt
+        | NONE => global_context ())
+    | NONE => global_context ())
   end;
 
 fun pp_thm th = Thm.pretty_thm_raw (guess_context ()) {quote = true, show_hyps = false} th;