proper context for extern operation: observe local options;
more uniform global_ctxt for pretty printing;

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

--- a/src/Pure/Proof/proof_checker.ML	Mon Dec 02 11:08:36 2024 +0100
+++ b/src/Pure/Proof/proof_checker.ML	Mon Dec 02 11:22:44 2024 +0100
@@ -72,7 +72,10 @@
   end;
 
 fun thm_of_proof thy =
-  let val lookup = lookup_thm thy in
+  let
+    val global_ctxt = Syntax.init_pretty_global thy;
+    val lookup = lookup_thm thy;
+  in
     fn prf =>
       let
         val prf_names =
@@ -96,9 +99,9 @@
                   if is_equal prop prop' then ()
                   else
                     error ("Duplicate use of theorem name " ^
-                      quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos
-                      ^ "\n" ^ Syntax.string_of_term_global thy prop
-                      ^ "\n\n" ^ Syntax.string_of_term_global thy prop');
+                      quote (Global_Theory.print_thm_name global_ctxt thm_name) ^ Position.here thm_pos
+                      ^ "\n" ^ Syntax.string_of_term global_ctxt prop
+                      ^ "\n\n" ^ Syntax.string_of_term global_ctxt prop');
               in thm_of_atom thm Ts end
 
           | thm_of _ _ (PAxm (name, _, SOME Ts)) =

--- a/src/Pure/Pure.thy	Mon Dec 02 11:08:36 2024 +0100
+++ b/src/Pure/Pure.thy	Mon Dec 02 11:22:44 2024 +0100
@@ -1378,10 +1378,8 @@
     "print theorem dependencies (immediate non-transitive)"
     (Parse.thms1 >> (fn args =>
       Toplevel.keep (fn st =>
-        let
-          val thy = Toplevel.theory_of st;
-          val ctxt = Toplevel.context_of st;
-        in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end)));
+        let val ctxt = Toplevel.context_of st
+        in Pretty.writeln (Thm_Deps.pretty_thm_deps ctxt (Attrib.eval_thms ctxt args)) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>thm_oracles\<close>

--- a/src/Pure/global_theory.ML	Mon Dec 02 11:08:36 2024 +0100
+++ b/src/Pure/global_theory.ML	Mon Dec 02 11:22:44 2024 +0100
@@ -14,8 +14,8 @@
   val alias_fact: binding -> string -> theory -> theory
   val hide_fact: bool -> string -> theory -> theory
   val dest_thms: bool -> theory list -> theory -> (Thm_Name.P * thm) list
-  val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T
-  val print_thm_name: theory -> Thm_Name.T -> string
+  val pretty_thm_name: Proof.context -> Thm_Name.T -> Pretty.T
+  val print_thm_name: Proof.context -> Thm_Name.T -> string
   val get_thm_names: theory -> Thm_Name.P Inttab.table
   val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.P) list
   val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.P option
@@ -88,7 +88,9 @@
   Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy)
   |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms);
 
-fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy);
+fun pretty_thm_name ctxt =
+  Facts.pretty_thm_name (Context.Proof ctxt) (facts_of (Proof_Context.theory_of ctxt));
+
 val print_thm_name = Pretty.string_of oo pretty_thm_name;
 
 
@@ -108,9 +110,11 @@
         else
           (case Inttab.lookup thm_names serial of
             SOME (thm_name', thm_pos') =>
-              raise THM ("Duplicate use of derivation identity for " ^
-                print_thm_name thy thm_name ^ Position.here thm_pos ^ " vs. " ^
-                print_thm_name thy thm_name' ^ Position.here thm_pos', 0, [thm])
+              let val thy_ctxt = Proof_Context.init_global thy in
+                raise THM ("Duplicate use of derivation identity for " ^
+                  print_thm_name thy_ctxt thm_name ^ Position.here thm_pos ^ " vs. " ^
+                  print_thm_name thy_ctxt thm_name' ^ Position.here thm_pos', 0, [thm])
+              end
           | NONE => Inttab.update (serial, (thm_name, thm_pos)) thm_names)));
 
 fun lazy_thm_names thy =

--- a/src/Pure/raw_simplifier.ML	Mon Dec 02 11:08:36 2024 +0100
+++ b/src/Pure/raw_simplifier.ML	Mon Dec 02 11:22:44 2024 +0100
@@ -481,10 +481,9 @@
 
 fun print_thm ctxt msg (name, th) =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val sffx =
       if Thm_Name.is_empty name then ""
-      else " " ^ quote (Global_Theory.print_thm_name thy name) ^ ":";
+      else " " ^ quote (Global_Theory.print_thm_name ctxt name) ^ ":";
   in print_term ctxt (msg ^ sffx) (Thm.full_prop_of th) end;
 
 fun print_thm0 ctxt msg th = print_thm ctxt msg (Thm_Name.empty, th);

--- a/src/Pure/thm_deps.ML	Mon Dec 02 11:08:36 2024 +0100
+++ b/src/Pure/thm_deps.ML	Mon Dec 02 11:22:44 2024 +0100
@@ -11,7 +11,7 @@
   val has_skip_proof: thm list -> bool
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
   val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
-  val pretty_thm_deps: theory -> thm list -> Pretty.T
+  val pretty_thm_deps: Proof.context -> thm list -> Pretty.T
   val unused_thms_cmd: theory list * theory list -> (Thm_Name.T * thm) list
 end;
 
@@ -71,10 +71,11 @@
       |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
   end;
 
-fun pretty_thm_deps thy thms =
+fun pretty_thm_deps ctxt thms =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val facts = Global_Theory.facts_of thy;
-    val extern_fact = Name_Space.extern_global thy (Facts.space_of facts);
+    val extern_fact = Name_Space.extern ctxt (Facts.space_of facts);
     val deps =
       (case try (thm_deps thy) thms of
         SOME deps => deps
@@ -83,7 +84,7 @@
       deps
       |> map (fn (_, thm_name as (name, _)) => (extern_fact name, thm_name))
       |> sort_by #1
-      |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name thy thm_name])
+      |> map (fn (_, thm_name) => Pretty.item [Global_Theory.pretty_thm_name ctxt thm_name])
   in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;