--- 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) =
--- 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]
--- 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;
--- 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);
--- 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 **)