# HG changeset patch
# User wenzelm
# Date 1717955382 -7200
# Node ID 718daea1cf99175d161b1fe5769decbcfaba1313
# Parent  c2537860ccf883178047a9bcc9c165654d853583
clarified modules;

diff -r c2537860ccf8 -r 718daea1cf99 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Sun Jun 09 15:31:33 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Sun Jun 09 19:49:42 2024 +0200
@@ -424,7 +424,7 @@
       end
 
     fun of_free (s, T) =
-      Proof_Context.print_name ctxt s ^ " :: " ^
+      Thy_Header.print_name' ctxt s ^ " :: " ^
       maybe_quote ctxt (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
 
     fun add_frees xs (s, ctxt) =
diff -r c2537860ccf8 -r 718daea1cf99 src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Sun Jun 09 15:31:33 2024 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Sun Jun 09 19:49:42 2024 +0200
@@ -91,7 +91,7 @@
     val fixes_s =
       if not is_for orelse null fixes then NONE
       else SOME ("for " ^ space_implode " "
-        (map (fn (v, _) => Proof_Context.print_name ctxt' v) fixes));
+        (map (fn (v, _) => Thy_Header.print_name' ctxt' v) fixes));
     val premises_s = if is_prems then SOME "premises prems" else NONE;
     val sh_s = if is_sh then SOME "sledgehammer" else NONE;
     val subgoal_s = map_filter I [SOME "subgoal", premises_s, fixes_s]
diff -r c2537860ccf8 -r 718daea1cf99 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Jun 09 15:31:33 2024 +0200
+++ b/src/Pure/Isar/element.ML	Sun Jun 09 19:49:42 2024 +0200
@@ -141,7 +141,7 @@
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_terms = separate (Pretty.keyword2 "and") o map prt_term;
     val prt_binding = Attrib.pretty_binding ctxt;
-    val prt_name = Proof_Context.pretty_name ctxt;
+    val prt_name = Thy_Header.pretty_name' ctxt;
 
     fun prt_show (a, ts) =
       Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
@@ -167,7 +167,7 @@
     val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
-    val prt_name = Proof_Context.pretty_name ctxt;
+    val prt_name = Thy_Header.pretty_name' ctxt;
 
     fun prt_binding (b, atts) =
       Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
@@ -228,7 +228,7 @@
   let val head =
     if Thm.has_name_hint th then
       Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
-        Proof_Context.pretty_name ctxt (Long_Name.base_name (#1 (Thm.get_name_hint th))),
+        Thy_Header.pretty_name' ctxt (Long_Name.base_name (#1 (Thm.get_name_hint th))),
         Pretty.str ":"]
     else Pretty.keyword1 kind
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
diff -r c2537860ccf8 -r 718daea1cf99 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jun 09 15:31:33 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 09 19:49:42 2024 +0200
@@ -65,8 +65,6 @@
   val pretty_thm_name: Proof.context -> Thm_Name.T -> Pretty.T
   val print_thm_name: Proof.context -> Thm_Name.T -> string
   val augment: term -> Proof.context -> Proof.context
-  val print_name: Proof.context -> string -> string
-  val pretty_name: Proof.context -> string -> Pretty.T
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val check_class: Proof.context -> xstring * Position.T -> class * Position.report list
@@ -442,9 +440,6 @@
 
 (** pretty printing **)
 
-val print_name = Token.print_name o Thy_Header.get_keywords';
-val pretty_name = Pretty.str oo print_name;
-
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
 fun pretty_fact_name ctxt a =
@@ -1506,7 +1501,7 @@
 
 fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) =
   let
-    val prt_name = pretty_name ctxt;
+    val prt_name = Thy_Header.pretty_name' ctxt;
     val prt_term = Syntax.pretty_term ctxt;
 
     fun prt_let (xi, t) = Pretty.block
@@ -1553,10 +1548,12 @@
     fun trim_name x = if Name.is_internal x then Name.clean x else "_";
     val trim_names = map trim_name #> drop_suffix (equal "_");
 
+    val print_name = Thy_Header.print_name' ctxt;
+
     fun print_case name xs =
       (case trim_names xs of
-        [] => print_name ctxt name
-      | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs'))));
+        [] => print_name name
+      | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs'))));
 
     fun is_case x t =
       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
diff -r c2537860ccf8 -r 718daea1cf99 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sun Jun 09 15:31:33 2024 +0200
+++ b/src/Pure/Thy/thy_header.ML	Sun Jun 09 19:49:42 2024 +0200
@@ -17,6 +17,11 @@
   val add_keywords: keywords -> theory -> theory
   val get_keywords: theory -> Keyword.keywords
   val get_keywords': Proof.context -> Keyword.keywords
+  val print_name: theory -> string -> string
+  val print_name': Proof.context -> string -> string
+  val pretty_name: theory -> string -> Pretty.T
+  val pretty_name': Proof.context -> string -> Pretty.T
+
   val ml_bootstrapN: string
   val ml_roots: string list
   val bootstrap_thys: string list
@@ -90,7 +95,7 @@
      (("ML", \<^here>), Keyword.command_spec (Keyword.thy_decl, ["ML"]))];
 
 
-(* theory data *)
+(* keywords *)
 
 structure Data = Theory_Data
 (
@@ -104,6 +109,12 @@
 val get_keywords = Data.get;
 val get_keywords' = get_keywords o Proof_Context.theory_of;
 
+val print_name = Token.print_name o get_keywords;
+val print_name' = Token.print_name o get_keywords';
+
+val pretty_name = Pretty.str oo print_name;
+val pretty_name' = Pretty.str oo print_name';
+
 
 
 (** concrete syntax **)