--- 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 =