diff -r fb49af893986 -r c32ebdcbe8ca src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Dec 02 11:08:36 2024 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Dec 02 11:22:44 2024 +0100
@@ -505,6 +505,8 @@
 fun extract thm_vss thy =
   let
     val thy' = add_syntax thy;
+    val global_ctxt = Syntax.init_pretty_global thy';
+    val print_thm_name = Global_Theory.print_thm_name global_ctxt;
 
     val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
       ExtractionData.get thy;
@@ -640,8 +642,7 @@
                   let
                     val _ = T = nullT orelse error "corr: internal error";
                     val _ =
-                      msg d ("Building correctness proof for " ^
-                        quote (Global_Theory.print_thm_name thy thm_name) ^
+                      msg d ("Building correctness proof for " ^ quote (print_thm_name thm_name) ^
                         (if null vs' then ""
                          else " (relevant variables: " ^ commas_quote vs' ^ ")"));
                     val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
@@ -670,8 +671,8 @@
             | SOME rs => (case find vs' rs of
                 SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
               | NONE => error ("corr: no realizer for instance of theorem " ^
-                  quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^
-                    Syntax.string_of_term_global thy'
+                  quote (print_thm_name thm_name) ^ ":\n" ^
+                    Syntax.string_of_term global_ctxt
                       (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
           end
 
@@ -686,7 +687,7 @@
               SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
                 defs)
             | NONE => error ("corr: no realizer for instance of axiom " ^
-                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
+                quote s ^ ":\n" ^ Syntax.string_of_term global_ctxt (Envir.beta_norm
                   (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))
           end
 
@@ -738,7 +739,7 @@
                 NONE =>
                   let
                     val _ =
-                      msg d ("Extracting " ^ quote (Global_Theory.print_thm_name thy' thm_name) ^
+                      msg d ("Extracting " ^ quote (print_thm_name thm_name) ^
                         (if null vs' then ""
                          else " (relevant variables: " ^ commas_quote vs' ^ ")"));
                     val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
@@ -790,8 +791,8 @@
             | SOME rs => (case find vs' rs of
                 SOME (t, _) => (subst_TVars tye' t, defs)
               | NONE => error ("extr: no realizer for instance of theorem " ^
-                  quote (Global_Theory.print_thm_name thy' thm_name) ^ ":\n" ^
-                    Syntax.string_of_term_global thy' (Envir.beta_norm
+                  quote (print_thm_name thm_name) ^ ":\n" ^
+                    Syntax.string_of_term global_ctxt (Envir.beta_norm
                     (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
           end
 
@@ -803,7 +804,7 @@
             case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
               SOME (t, _) => (subst_TVars tye' t, defs)
             | NONE => error ("extr: no realizer for instance of axiom " ^
-                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
+                quote s ^ ":\n" ^ Syntax.string_of_term global_ctxt (Envir.beta_norm
                   (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))
           end
 
@@ -817,7 +818,7 @@
         val name = Thm.derivation_name thm;
         val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else ();
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
-          quote (Global_Theory.print_thm_name thy' name) ^ " has no computational content")
+          quote (print_thm_name name) ^ " has no computational content")
       in Proofterm.reconstruct_proof thy' prop prf end;
 
     val defs =