# HG changeset patch
# User wenzelm
# Date 1733135813 -3600
# Node ID db073d1733ab5528a8b0f18bb0b687c899a68a85
# Parent  c32ebdcbe8ca72131a48349a14f8188d34bbd3f7
clarified signature: uniform context;

diff -r c32ebdcbe8ca -r db073d1733ab src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Dec 02 11:22:44 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Dec 02 11:36:53 2024 +0100
@@ -434,7 +434,7 @@
       in (markups, xname) end;
 
 fun pretty_thm_name ctxt (name, i) =
-  Facts.pretty_thm_name (Context.Proof ctxt) (facts_of_fact ctxt name) (name, i);
+  Facts.pretty_thm_name ctxt (facts_of_fact ctxt name) (name, i);
 
 val print_thm_name = Pretty.string_of oo pretty_thm_name;
 
diff -r c32ebdcbe8ca -r db073d1733ab src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Dec 02 11:22:44 2024 +0100
+++ b/src/Pure/facts.ML	Mon Dec 02 11:36:53 2024 +0100
@@ -30,7 +30,7 @@
   val intern: T -> xstring -> string
   val extern: Proof.context -> T -> string -> xstring
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
-  val pretty_thm_name: Context.generic -> T -> Thm_Name.T -> Pretty.T
+  val pretty_thm_name: Proof.context -> T -> Thm_Name.T -> Pretty.T
   val defined: T -> string -> bool
   val is_dynamic: T -> string -> bool
   val lookup: Context.generic -> T -> string -> {dynamic: bool, thms: thm list} option
@@ -174,9 +174,9 @@
 fun extern ctxt = Name_Space.extern ctxt o space_of;
 fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
 
-fun pretty_thm_name context facts thm_name =
+fun pretty_thm_name ctxt facts thm_name =
   let
-    val prfx = Thm_Name.print_prefix context (space_of facts) thm_name;
+    val prfx = Thm_Name.print_prefix ctxt (space_of facts) thm_name;
     val sffx = Thm_Name.print_suffix thm_name;
   in Pretty.block [Pretty.mark_str prfx, Pretty.str sffx] end;
 
diff -r c32ebdcbe8ca -r db073d1733ab src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Mon Dec 02 11:22:44 2024 +0100
+++ b/src/Pure/global_theory.ML	Mon Dec 02 11:36:53 2024 +0100
@@ -89,7 +89,7 @@
   |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms);
 
 fun pretty_thm_name ctxt =
-  Facts.pretty_thm_name (Context.Proof ctxt) (facts_of (Proof_Context.theory_of ctxt));
+  Facts.pretty_thm_name ctxt (facts_of (Proof_Context.theory_of ctxt));
 
 val print_thm_name = Pretty.string_of oo pretty_thm_name;
 
diff -r c32ebdcbe8ca -r db073d1733ab src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Mon Dec 02 11:22:44 2024 +0100
+++ b/src/Pure/thm_name.ML	Mon Dec 02 11:36:53 2024 +0100
@@ -23,7 +23,7 @@
   val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
 
   val parse: string -> T
-  val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string
+  val print_prefix: Proof.context -> Name_Space.T -> T -> Markup.T * string
   val print_suffix: T -> string
   val print: T -> string
   val print_pos: P -> string
@@ -99,9 +99,9 @@
 
 (* print *)
 
-fun print_prefix context space ((name, _): T) =
+fun print_prefix ctxt space ((name, _): T) =
   if name = "" then (Markup.empty, "")
-  else (Name_Space.markup space name, Name_Space.extern_generic context space name);
+  else (Name_Space.markup space name, Name_Space.extern ctxt space name);
 
 fun print_suffix (name, index) =
   if name = "" orelse index = 0 then ""