# HG changeset patch # User wenzelm # Date 1717939893 -7200 # Node ID c2537860ccf883178047a9bcc9c165654d853583 # Parent 95b51df1382e79187d0385bd30f7be0d764225a0 more accurate thm "name_hint", using Thm_Name.T; diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Jun 09 15:31:33 2024 +0200 @@ -235,7 +235,7 @@ val forbidden_consts = [\<^const_name>\Pure.type\] -fun is_forbidden_theorem (s, th) = +fun is_forbidden_theorem ((s, _): Thm_Name.T, th) = let val consts = Term.add_const_names (Thm.prop_of th) [] in exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse exists (member (op =) forbidden_consts) consts orelse @@ -421,13 +421,13 @@ ^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")" (*^ "\n" ^ string_of_reports reports*) in - "mutant of " ^ thm_name ^ ":\n" ^ + "mutant of " ^ Thm_Name.short thm_name ^ ":\n" ^ YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results) end fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = - thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^ + Thm_Name.short thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^ Syntax.string_of_term_global thy t ^ "\n" ^ cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n" diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Sun Jun 09 15:31:33 2024 +0200 @@ -151,7 +151,7 @@ String.isSuffix "_raw" name fun theorems_of thy = - filter (fn (name, th) => + filter (fn ((name, _), th) => not (is_forbidden_theorem name) andalso Thm.theory_long_name th = Context.theory_long_name thy) (Global_Theory.all_thms_of thy true) @@ -186,7 +186,7 @@ val (nondef_ts, def_ts, _, _, _, _) = Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt []) neg_t - val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts) + val res = Thm_Name.print name ^ ": " ^ check_formulas (nondef_ts, def_ts) in File.append path (res ^ "\n"); writeln res end handle Timeout.TIMEOUT _ => () in thy |> theorems_of |> List.app check_theorem end diff -r 95b51df1382e -r c2537860ccf8 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Sun Jun 09 15:31:33 2024 +0200 @@ -164,19 +164,19 @@ val problem = facts |> map (fn ((_, loc), th) => - ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) + ((Thm_Name.short (Thm.get_name_hint th), loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt)) |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true [] \<^prop>\False\ |> #1 |> sort_by (heading_sort_key o fst) val prelude = fst (split_last problem) - val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts + val name_tabs = Sledgehammer_Fact.build_name_tables (Thm_Name.short o Thm.get_name_hint) facts val infers = if infer_policy = No_Inferences then [] else facts |> map (fn (_, th) => - (fact_name_of (Thm.get_name_hint th), + (fact_name_of (Thm_Name.short (Thm.get_name_hint th)), th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs) |> these |> map fact_name_of)) val all_problem_names = @@ -295,7 +295,7 @@ #> chop_maximal_groups (op = o apply2 theory_name_of_fact) #> map (`(include_base_name_of_fact o hd))) - val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts) + val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm_Name.short (Thm.get_name_hint th), fact)) facts) fun write_prelude () = let val ss = lines_of_atp_problem format (K []) prelude in @@ -318,7 +318,7 @@ val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt (Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts in - map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo + map (suffix "\n" o fact_name_of o Thm_Name.short o Thm.get_name_hint o snd) mepo end fun write_problem_files _ _ _ _ [] = () diff -r 95b51df1382e -r c2537860ccf8 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/TPTP/mash_export.ML Sun Jun 09 15:31:33 2024 +0200 @@ -172,7 +172,7 @@ j mod step <> 0 orelse Thm.legacy_get_kind th = "" orelse null (the_list isar_deps) orelse - is_blacklisted_or_something (Thm.get_name_hint th) + is_blacklisted_or_something (Thm_Name.short (Thm.get_name_hint th)) fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name = let diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Sun Jun 09 15:31:33 2024 +0200 @@ -417,7 +417,7 @@ fun short_thm_name ctxt th = let - val long = Thm.get_name_hint th + val long = Thm_Name.short (Thm.get_name_hint th) val short = Long_Name.base_name long in (case try (singleton (Attrib.eval_thms ctxt)) (Facts.named short, []) of diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Sun Jun 09 15:31:33 2024 +0200 @@ -459,7 +459,7 @@ (*Use "theorem naming" to label the clauses*) fun name_thms label = let fun name1 th (k, ths) = - (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) + (k-1, Thm.put_name_hint (label ^ string_of_int k, 0) th :: ths) in fn ths => #2 (fold_rev name1 ths (length ths, [])) end; (*Is the given disjunction an all-negative support clause?*) diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Sun Jun 09 15:31:33 2024 +0200 @@ -214,7 +214,8 @@ val _ = unused := maps (#2 o #2) unused_th_cls_pairs; val _ = if not (null unused_th_cls_pairs) then - verbose_warning ctxt ("Unused theorems: " ^ commas_quote (map #1 unused_th_cls_pairs)) + verbose_warning ctxt ("Unused theorems: " ^ + commas_quote (map (Proof_Context.print_thm_name ctxt o #1) unused_th_cls_pairs)) else (); val _ = if not (null cls) andalso not (have_common_thm ctxt used cls) then diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 09 15:31:33 2024 +0200 @@ -305,11 +305,11 @@ if Inttab.defined seen i then (x, seen) else let - val name = Thm_Name.short (Proofterm.thm_node_name thm_node); + val name = Proofterm.thm_node_name thm_node; val prop = Proofterm.thm_node_prop thm_node; val body = Future.join (Proofterm.thm_node_body thm_node); val (x', seen') = - app (n + (if name = "" then 0 else 1)) body + app (n + (if Thm_Name.is_empty name then 0 else 1)) body (x, Inttab.update (i, ()) seen); in (x' |> n = 0 ? f (name, prop, body), seen') end); in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; @@ -319,7 +319,7 @@ fun theorems_in_proof_term thy thm = let val all_thms = Global_Theory.all_thms_of thy true; - fun collect (s, _, _) = if s <> "" then insert (op =) s else I; + fun collect (name, _, _) = if Thm_Name.is_empty name then I else insert (op =) name; fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; fun resolve_thms names = map_filter (member_of names) all_thms; in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Mirabelle/mirabelle_metis.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sun Jun 09 15:31:33 2024 +0200 @@ -19,7 +19,7 @@ fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts); in (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") - |> not (null names) ? suffix (":\n" ^ commas names) + |> not (null names) ? suffix (":\n" ^ commas (map Thm_Name.short names)) end in ("", {run = run, finalize = K ""}) end diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Quickcheck/find_unused_assms.ML --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sun Jun 09 15:31:33 2024 +0200 @@ -7,7 +7,7 @@ signature FIND_UNUSED_ASSMS = sig val check_unused_assms: Proof.context -> string * thm -> string * int list list option - val find_unused_assms: Proof.context -> string -> (string * int list list option) list + val find_unused_assms: Proof.context -> string -> (Thm_Name.T * int list list option) list val print_unused_assms: Proof.context -> string option -> unit end @@ -71,8 +71,8 @@ val thy = Proof_Context.theory_of ctxt val all_thms = thms_of thy thy_name - |> filter (fn (name, _) => Long_Name.count name = 2) (* FIXME !? *) - |> sort_by #1 + |> filter (fn ((name, _), _) => Long_Name.count name = 2) (* FIXME !? *) + |> sort (Thm_Name.ord o apply2 #1) val check = check_unused_assms ctxt in rev (Par_List.map check all_thms) end @@ -86,8 +86,8 @@ (flat (separate [Pretty.str " and", Pretty.brk 1] (map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is)))) -fun pretty_thm (name, set_of_indexes) = - Pretty.block (Pretty.str name :: Pretty.str ":" :: Pretty.brk 1 :: +fun pretty_thm ctxt (name, set_of_indexes) = + Pretty.block (Proof_Context.pretty_thm_name ctxt name :: Pretty.str ":" :: Pretty.brk 1 :: Pretty.str "unnecessary assumption " :: separate (Pretty.str " or ") (map pretty_indexes set_of_indexes)) @@ -112,7 +112,7 @@ string_of_int total ^ " total) in the theory " ^ quote thy_name in [Pretty.str (msg ^ ":"), Pretty.str ""] @ - map pretty_thm with_superfluous_assumptions @ + map (pretty_thm ctxt) with_superfluous_assumptions @ [Pretty.str "", Pretty.str end_msg] end |> Pretty.writeln_chunks diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Jun 09 15:31:33 2024 +0200 @@ -223,7 +223,7 @@ fun is_that_fact th = exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th) - andalso String.isSuffix sep_that (Thm.get_name_hint th) + andalso String.isSuffix sep_that (Thm_Name.short (Thm.get_name_hint th)) datatype interest = Deal_Breaker | Interesting | Boring @@ -359,7 +359,7 @@ let fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (Thm.prop_of th)), th) fun add_plain canon alias = - Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias)) + Symtab.update (Thm_Name.short (Thm.get_name_hint alias), name_of (if_thm_before canon alias)) fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name) val prop_tab = fold cons_thm facts Termtab.empty diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 09 15:31:33 2024 +0200 @@ -789,7 +789,7 @@ fun nickname_of_thm th = if Thm.has_name_hint th then - let val hint = Thm.get_name_hint th in + let val hint = Thm_Name.short (Thm.get_name_hint th) in (* There must be a better way to detect local facts. *) (case Long_Name.dest_local hint of SOME suf => diff -r 95b51df1382e -r c2537860ccf8 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Jun 09 15:31:33 2024 +0200 @@ -108,7 +108,8 @@ NONE => NONE | SOME body => let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in - SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm_body body)) + SOME (fold_body_thm max_thms (Thm_Name.short (Thm.get_name_hint th)) map_names + (Proofterm.strip_thm_body body)) handle TOO_MANY () => NONE end) diff -r 95b51df1382e -r c2537860ccf8 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/Pure/Isar/element.ML Sun Jun 09 15:31:33 2024 +0200 @@ -228,7 +228,8 @@ 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 (Thm.get_name_hint th)), Pretty.str ":"] + Proof_Context.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 95b51df1382e -r c2537860ccf8 src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/Pure/Proof/proof_checker.ML Sun Jun 09 15:31:33 2024 +0200 @@ -16,10 +16,13 @@ (***** construct a theorem out of a proof term *****) fun lookup_thm thy = - let val tab = Symtab.build (Global_Theory.all_thms_of thy true |> fold_rev Symtab.update) in - fn s => - (case Symtab.lookup tab s of - NONE => error ("Unknown theorem " ^ quote s) + let + val tab = + Thm_Name.Table.build (Global_Theory.all_thms_of thy true |> fold_rev Thm_Name.Table.update); + in + fn name => + (case Thm_Name.Table.lookup tab name of + NONE => error ("Unknown theorem " ^ quote (Thm_Name.print name)) | SOME thm => thm) end; @@ -87,8 +90,7 @@ fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) = let - val name = Thm_Name.short thm_name; - val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name)); + val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup thm_name)); val prop = Thm.prop_of thm; val _ = if is_equal prop prop' then () diff -r 95b51df1382e -r c2537860ccf8 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sun Jun 09 15:31:33 2024 +0200 @@ -143,7 +143,7 @@ fun proof_of_term thy ty = let - val thms = Global_Theory.all_thms_of thy true; + val thms = Global_Theory.all_thms_of thy true |> map (apfst Thm_Name.short); val axms = Theory.all_axioms_of thy; fun mk_term t = (if ty then I else map_types (K dummyT)) @@ -200,7 +200,8 @@ fun read_term thy topsort = let - val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true)); + val thm_names = + filter_out (fn s => s = "") (map (Thm_Name.short o fst) (Global_Theory.all_thms_of thy true)); val axm_names = map fst (Theory.all_axioms_of thy); val ctxt = thy |> add_proof_syntax diff -r 95b51df1382e -r c2537860ccf8 src/Pure/Tools/simplifier_trace.ML --- a/src/Pure/Tools/simplifier_trace.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/Pure/Tools/simplifier_trace.ML Sun Jun 09 15:31:33 2024 +0200 @@ -230,7 +230,7 @@ let (* FIXME pretty printing via Proof_Context.pretty_fact *) val pretty_thm = Pretty.block - [Pretty.str ("Instance of " ^ name ^ ":"), + [Pretty.str ("Instance of " ^ Proof_Context.print_thm_name ctxt name ^ ":"), Pretty.brk 1, Syntax.pretty_term ctxt (Thm.prop_of thm)] @@ -319,7 +319,7 @@ val pretty_thm = (* FIXME pretty printing via Proof_Context.pretty_fact *) Pretty.block - [Pretty.str ("In an instance of " ^ name ^ ":"), + [Pretty.str ("In an instance of " ^ Proof_Context.print_thm_name ctxt name ^ ":"), Pretty.brk 1, Syntax.pretty_term ctxt (Thm.prop_of thm)] diff -r 95b51df1382e -r c2537860ccf8 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/Pure/global_theory.ML Sun Jun 09 15:31:33 2024 +0200 @@ -23,7 +23,7 @@ val get_thms: theory -> xstring -> thm list val get_thm: theory -> xstring -> thm val transfer_theories: theory -> thm -> thm - val all_thms_of: theory -> bool -> (string * thm) list + val all_thms_of: theory -> bool -> (Thm_Name.T * thm) list val get_thm_name: theory -> Thm_Name.T * Position.T -> thm type name_flags val unnamed: name_flags @@ -259,7 +259,7 @@ |> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ? Thm.name_derivation (name, pos) |> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ? - Thm.put_name_hint (Thm_Name.short name))); + Thm.put_name_hint name)); end; diff -r 95b51df1382e -r c2537860ccf8 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/Pure/more_thm.ML Sun Jun 09 15:31:33 2024 +0200 @@ -88,8 +88,8 @@ val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding val make_def_binding: bool -> Binding.binding -> Binding.binding val has_name_hint: thm -> bool - val get_name_hint: thm -> string - val put_name_hint: string -> thm -> thm + val get_name_hint: thm -> Thm_Name.T + val put_name_hint: Thm_Name.T -> thm -> thm val theoremK: string val legacy_get_kind: thm -> string val kind_rule: string -> thm -> thm @@ -607,10 +607,10 @@ (* unofficial theorem names *) fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; -fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); -fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; +fun the_name_hint thm = Thm_Name.parse (the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN)); +fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else ("??.unknown", 0); -fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); +fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, Thm_Name.print name); (* theorem kinds *) diff -r 95b51df1382e -r c2537860ccf8 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Sun Jun 09 15:11:07 2024 +0200 +++ b/src/Pure/raw_simplifier.ML Sun Jun 09 15:31:33 2024 +0200 @@ -27,7 +27,7 @@ val empty_ss: simpset val merge_ss: simpset * simpset -> simpset val dest_ss: simpset -> - {simps: (string * thm) list, + {simps: (Thm_Name.T * thm) list, procs: (string * term list) list, congs: (cong_name * thm) list, weak_congs: cong_name list, @@ -133,7 +133,7 @@ type rrule = {thm: thm, (*the rewrite rule*) - name: string, (*name of theorem from which rewrite rule was extracted*) + name: Thm_Name.T, (*name of theorem from which rewrite rule was extracted*) lhs: term, (*the left-hand side*) elhs: cterm, (*the eta-contracted lhs*) extra: bool, (*extra variables outside of elhs*) @@ -443,10 +443,15 @@ fun print_term ctxt s t = s ^ "\n" ^ Syntax.string_of_term ctxt t; -fun print_thm ctxt s (name, th) = - print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th); +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) ^ ":"; + in print_term ctxt (msg ^ sffx) (Thm.full_prop_of th) end; -fun print_thm0 ctxt msg th = print_thm ctxt msg ("", th); +fun print_thm0 ctxt msg th = print_thm ctxt msg (Thm_Name.empty, th); @@ -931,7 +936,7 @@ in if rewrite_rule_extra_vars prems lhs rhs then (cond_warning ctxt (fn () => print_thm0 ctxt "Extra vars on rhs:" thm); []) - else [mk_rrule2 {thm = thm', name = "", lhs = lhs, elhs = elhs, perm = false}] + else [mk_rrule2 {thm = thm', name = Thm_Name.empty, lhs = lhs, elhs = elhs, perm = false}] end;