diff -r ee9785abbcd6 -r a6bd716a6124 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/Isar/proof_display.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -44,9 +44,8 @@
   (case Context.get_generic_context () of
     SOME (Context.Proof ctxt) => ctxt
   | SOME (Context.Theory thy) =>
-      (case try Syntax.init_pretty_global thy of
-        SOME ctxt => ctxt
-      | NONE => Syntax.init_pretty_global (mk_thy ()))
+      try Syntax.init_pretty_global thy
+      |> \<^if_none>\<open>Syntax.init_pretty_global (mk_thy ())\<close>
   | NONE => Syntax.init_pretty_global (mk_thy ()));
 
 fun pp_thm mk_thy th =