# HG changeset patch # User wenzelm # Date 1681984654 -7200 # Node ID 5db014c36f425ce341eb9a94dc43f5b66cdad18d # Parent 3c837f8c8ed5b25991bcde4f079fa1c8fd29b170 clarified signature: explicitly distinguish theory_base_name vs. theory_long_name; diff -r 3c837f8c8ed5 -r 5db014c36f42 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Thu Apr 20 11:57:34 2023 +0200 @@ -331,7 +331,7 @@ fun thms_of all thy = filter - (fn th => (all orelse Thm.theory_name th = Context.theory_name thy) + (fn th => (all orelse Thm.theory_base_name th = Context.theory_base_name thy) (* andalso is_executable_thm thy th *)) (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false))) diff -r 3c837f8c8ed5 -r 5db014c36f42 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Apr 19 23:27:55 2023 +0200 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Apr 20 11:57:34 2023 +0200 @@ -153,7 +153,7 @@ fun theorems_of thy = filter (fn (name, th) => not (is_forbidden_theorem name) andalso - Thm.theory_name th = Context.theory_name thy) + Thm.theory_base_name th = Context.theory_base_name thy) (Global_Theory.all_thms_of thy true) fun check_formulas tsp = @@ -175,7 +175,7 @@ fun check_theory thy = let - val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode) + val path = File.tmp_path (Context.theory_base_name thy ^ ".out" |> Path.explode) val _ = File.write path "" fun check_theorem (name, th) = let diff -r 3c837f8c8ed5 -r 5db014c36f42 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/HOL/TPTP/mash_export.ML Thu Apr 20 11:57:34 2023 +0200 @@ -58,7 +58,7 @@ | _ => ("", [])) fun has_thm_thy th thy = - Context.theory_name thy = Thm.theory_name th + Context.theory_base_name thy = Thm.theory_base_name th fun has_thys thys th = exists (has_thm_thy th) thys @@ -98,7 +98,7 @@ fun do_fact ((_, stature), th) = let val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] + val feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th] val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n" in File.append path s @@ -187,14 +187,14 @@ val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val isar_deps = isar_dependencies_of name_tabs th val do_query = not (is_bad_query ctxt step j th isar_deps) - val goal_feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] + val goal_feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th] val access_facts = filter_accessible_from th new_facts @ old_facts val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps fun extra_features_of (((_, stature), th), weight) = [Thm.prop_of th] - |> features_of ctxt (Thm.theory_name th) stature + |> features_of ctxt (Thm.theory_base_name th) stature |> map (rpair (weight * extra_feature_factor)) val query = @@ -261,7 +261,7 @@ val suggs = old_facts |> filter_accessible_from th - |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name th) + |> mepo_or_mash_suggested_facts ctxt (Thm.theory_base_name th) params max_suggs hyp_ts concl_t |> map (nickname_of_thm o snd) in diff -r 3c837f8c8ed5 -r 5db014c36f42 src/HOL/Tools/Quickcheck/find_unused_assms.ML --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Thu Apr 20 11:57:34 2023 +0200 @@ -16,7 +16,7 @@ fun thms_of thy thy_name = Global_Theory.all_thms_of thy false - |> filter (fn (_, th) => Thm.theory_name th = thy_name) + |> filter (fn (_, th) => Thm.theory_base_name th = thy_name) fun do_while P f s list = if P s then @@ -95,7 +95,8 @@ fun print_unused_assms ctxt opt_thy_name = let - val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name + val thy_name = + the_default (Context.theory_base_name (Proof_Context.theory_of ctxt)) opt_thy_name val results = find_unused_assms ctxt thy_name val total = length results val with_assumptions = length (filter (is_some o snd) results) diff -r 3c837f8c8ed5 -r 5db014c36f42 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Apr 20 11:57:34 2023 +0200 @@ -796,7 +796,7 @@ (* There must be a better way to detect local facts. *) (case Long_Name.dest_local hint of SOME suf => - Long_Name.implode [Thm.theory_name th, suf, crude_printed_term 25 (Thm.prop_of th)] + Long_Name.implode [Thm.theory_base_name th, suf, crude_printed_term 25 (Thm.prop_of th)] | NONE => hint) end else @@ -820,9 +820,9 @@ fun crude_thm_ord ctxt = let val ancestor_lengths = - fold (fn thy => Symtab.update (Context.theory_name thy, length (Context.ancestors_of thy))) + fold (fn thy => Symtab.update (Context.theory_base_name thy, length (Context.ancestors_of thy))) (Theory.nodes_of (Proof_Context.theory_of ctxt)) Symtab.empty - val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name + val ancestor_length = Symtab.lookup ancestor_lengths o Context.theory_id_name {long = false} fun crude_theory_ord p = if Context.eq_thy_id p then EQUAL @@ -832,9 +832,9 @@ (case apply2 ancestor_length p of (SOME m, SOME n) => (case int_ord (m, n) of - EQUAL => string_ord (apply2 Context.theory_id_name p) + EQUAL => string_ord (apply2 (Context.theory_id_name {long = false}) p) | ord => ord) - | _ => string_ord (apply2 Context.theory_id_name p)) + | _ => string_ord (apply2 (Context.theory_id_name {long = false}) p)) in fn p => (case crude_theory_ord (apply2 Thm.theory_id p) of @@ -1125,7 +1125,7 @@ val chunks = app_hd (cons th) chunks val chunks_and_parents' = if thm_less_eq (th, th') andalso - Thm.theory_name th = Thm.theory_name th' + Thm.theory_base_name th = Thm.theory_base_name th' then (chunks, [nickname_of_thm th]) else chunks_and_parents_for chunks th' in @@ -1172,11 +1172,11 @@ val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts - fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name th + fun fact_has_right_theory (_, th) = thy_name = Thm.theory_base_name th fun chained_or_extra_features_of factor (((_, stature), th), weight) = [Thm.prop_of th] - |> features_of ctxt (Thm.theory_name th) stature + |> features_of ctxt (Thm.theory_base_name th) stature |> map (rpair (weight * factor)) in (case get_state ctxt of @@ -1283,7 +1283,7 @@ launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt - val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t] + val feats = features_of ctxt (Context.theory_base_name thy) (Local, General) [t] in map_state ctxt (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} => @@ -1395,7 +1395,7 @@ (learns, (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th] + val feats = features_of ctxt (Thm.theory_base_name th) stature [Thm.prop_of th] val deps = these (deps_of status th) val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1 val learns = (name, parents, feats, deps) :: learns @@ -1544,7 +1544,7 @@ [("", [])] else let - val thy_name = Context.theory_name (Proof_Context.theory_of ctxt) + val thy_name = Context.theory_base_name (Proof_Context.theory_of ctxt) fun maybe_launch_thread exact min_num_facts_to_learn = if not (Async_Manager_Legacy.has_running_threads MaShN) andalso diff -r 3c837f8c8ed5 -r 5db014c36f42 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Apr 20 11:57:34 2023 +0200 @@ -220,7 +220,7 @@ t fun theory_const_prop_of fudge th = - theory_constify fudge (Thm.theory_name th) (Thm.prop_of th) + theory_constify fudge (Thm.theory_base_name th) (Thm.prop_of th) fun pair_consts_fact thy fudge fact = (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of @@ -546,7 +546,7 @@ [] else relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts - (concl_t |> theory_constify fudge (Context.theory_name thy))) + (concl_t |> theory_constify fudge (Context.theory_base_name thy))) |> map fact_of_lazy_fact end diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/Isar/named_target.ML Thu Apr 20 11:57:34 2023 +0200 @@ -97,7 +97,7 @@ theory_registration = Generic_Target.theory_registration, locale_dependency = fn _ => error "Not possible in theory target", pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, - Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]} + Pretty.str (Context.theory_base_name (Proof_Context.theory_of ctxt))]]} | operations (Locale locale) = {define = Generic_Target.define (locale_foundation locale), notes = Generic_Target.notes (Generic_Target.locale_target_notes locale), diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Thu Apr 20 11:57:34 2023 +0200 @@ -112,7 +112,7 @@ (* maintain commands *) fun add_command name cmd thy = - if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy + if member (op =) Thy_Header.bootstrap_thys (Context.theory_base_name thy) then thy else let val _ = diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 20 11:57:34 2023 +0200 @@ -10,7 +10,7 @@ sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context - val get_global: theory -> string -> Proof.context + val get_global: {long: bool} -> theory -> string -> Proof.context type mode val mode_default: mode val mode_pattern: mode diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Apr 20 11:57:34 2023 +0200 @@ -162,7 +162,7 @@ Toplevel => (case previous_theory_of state of NONE => "at top level" - | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy)) + | SOME thy => "at top level, result theory " ^ quote (Context.theory_base_name thy)) | Theory (Context.Theory _) => "in theory mode" | Theory (Context.Proof _) => "in local theory mode" | Proof _ => "in proof mode" diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Thu Apr 20 11:57:34 2023 +0200 @@ -65,7 +65,7 @@ ML_Antiquotation.value_embedded \<^binding>\theory_context\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); - "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ + "Proof_Context.get_global {long = false} (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))) #> ML_Antiquotation.inline \<^binding>\context\ diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/Thy/export_theory.ML Thu Apr 20 11:57:34 2023 +0200 @@ -414,7 +414,7 @@ get_dependencies parents thy |> map_index (fn (i, dep) => let val xname = string_of_int (i + 1); - val name = Long_Name.implode [Context.theory_name thy, xname]; + val name = Long_Name.implode [Context.theory_base_name thy, xname]; val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep)); val body = encode_locale_dependency dep; in XML.Elem (markup, body) end) diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/Thy/thy_info.ML Thu Apr 20 11:57:34 2023 +0200 @@ -65,7 +65,7 @@ else let val keywords = Thy_Header.get_keywords thy; - val thy_name = Context.theory_name thy; + val thy_name = Context.theory_base_name thy; val latex = Document_Output.present_thy options keywords thy_name segments; in if Options.string options "document" = "false" then () diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/Tools/thy_deps.ML --- a/src/Pure/Tools/thy_deps.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/Tools/thy_deps.ML Thu Apr 20 11:57:34 2023 +0200 @@ -27,8 +27,8 @@ SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs) | NONE => K true); fun node thy = - ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []), - map Context.theory_name (filter pred (Theory.parents_of thy))); + ((Context.theory_base_name thy, Graph_Display.content_node (Context.theory_base_name thy) []), + map Context.theory_base_name (filter pred (Theory.parents_of thy))); in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end; val thy_deps = diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/context.ML --- a/src/Pure/context.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/context.ML Thu Apr 20 11:57:34 2023 +0200 @@ -20,7 +20,7 @@ sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context - val get_global: theory -> string -> Proof.context + val get_global: {long: bool} -> theory -> string -> Proof.context end end; @@ -34,11 +34,10 @@ val parents_of: theory -> theory list val ancestors_of: theory -> theory list val theory_id_ord: theory_id ord - val theory_id_long_name: theory_id -> string - val theory_id_name: theory_id -> string + val theory_id_name: {long: bool} -> theory_id -> string val theory_long_name: theory -> string - val theory_name: theory -> string - val theory_name': {long: bool} -> theory -> string + val theory_base_name: theory -> string + val theory_name: {long: bool} -> theory -> string val theory_identifier: theory -> serial val PureN: string val pretty_thy: theory -> Pretty.T @@ -166,12 +165,13 @@ val theory_id_stage = #stage o rep_theory_id; val theory_id_final = stage_final o theory_id_stage; val theory_id_ord = int_ord o apply2 (#id o rep_theory_id); -val theory_id_long_name = #name o rep_theory_id; -val theory_id_name = Long_Name.base_name o theory_id_long_name; +fun theory_id_name {long} thy_id = + let val name = #name (rep_theory_id thy_id) + in if long then name else Long_Name.base_name name end; val theory_long_name = #name o identity_of; -val theory_name = Long_Name.base_name o theory_long_name; -fun theory_name' {long} = if long then theory_long_name else theory_name; +val theory_base_name = Long_Name.base_name o theory_long_name; +fun theory_name {long} = if long then theory_long_name else theory_base_name; val theory_identifier = #id o identity_of; val parents_of = #parents o ancestry_of; @@ -183,8 +183,10 @@ val PureN = "Pure"; fun display_name thy_id = - if theory_id_final thy_id then theory_id_name thy_id - else theory_id_name thy_id ^ ":" ^ string_of_int (theory_id_stage thy_id); + let + val name = theory_id_name {long = false} thy_id; + val final = theory_id_final thy_id; + in if final then name else name ^ ":" ^ string_of_int (theory_id_stage thy_id) end; fun display_names thy = let @@ -204,8 +206,8 @@ in Pretty.str_list "{" "}" abbrev end; fun get_theory long thy name = - if theory_name' long thy <> name then - (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of + if theory_name long thy <> name then + (case find_first (fn thy' => theory_name long thy' = name) (ancestors_of thy) of SOME thy' => thy' | NONE => error ("Unknown ancestor theory " ^ quote name)) else if theory_id_final (theory_id thy) then thy @@ -238,7 +240,7 @@ fun eq_thy_consistent (thy1, thy2) = eq_thy (thy1, thy2) orelse - (theory_name thy1 = theory_name thy2 andalso + (theory_base_name thy1 = theory_base_name thy2 andalso raise THEORY ("Duplicate theory name", [thy1, thy2])); fun extend_ancestors thy thys = @@ -513,7 +515,7 @@ struct fun theory_of (Proof.Context (_, thy)) = thy; fun init_global thy = Proof.Context (init_data thy, thy); - fun get_global thy name = init_global (get_theory {long = false} thy name); + fun get_global long thy name = init_global (get_theory long thy name); end; structure Proof_Data = diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/global_theory.ML Thu Apr 20 11:57:34 2023 +0200 @@ -172,9 +172,9 @@ let val theories = Symtab.build (Theory.nodes_of thy |> fold (fn thy' => - Symtab.update (Context.theory_name thy', thy'))); + Symtab.update (Context.theory_base_name thy', thy'))); fun transfer th = - Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th; + Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_base_name th))) th; in transfer end; fun all_thms_of thy verbose = diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/proofterm.ML Thu Apr 20 11:57:34 2023 +0200 @@ -2137,7 +2137,7 @@ fun export_standard_enabled () = Options.default_bool "export_standard_proofs"; fun export_proof_boxes_required thy = - Context.theory_name thy = Context.PureN orelse + Context.theory_base_name thy = Context.PureN orelse (export_enabled () andalso not (export_standard_enabled ())); fun export_proof_boxes bodies = diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/sign.ML Thu Apr 20 11:57:34 2023 +0200 @@ -514,7 +514,7 @@ val mandatory_path = map_naming o Name_Space.mandatory_path; val qualified_path = map_naming oo Name_Space.qualified_path; -fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy); +fun local_path thy = thy |> root_path |> add_path (Context.theory_base_name thy); fun init_naming thy = let diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/theory.ML --- a/src/Pure/theory.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/theory.ML Thu Apr 20 11:57:34 2023 +0200 @@ -143,7 +143,7 @@ val completion_report = Completion.make_report (name, pos) (fn completed => - map (Context.theory_name' long) (ancestors_of thy) + map (Context.theory_name long) (ancestors_of thy) |> filter (completed o Long_Name.base_name) |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/thm.ML Thu Apr 20 11:57:34 2023 +0200 @@ -66,7 +66,9 @@ val terms_of_tpairs: (term * term) list -> term list val full_prop_of: thm -> term val theory_id: thm -> Context.theory_id - val theory_name: thm -> string + val theory_name: {long: bool} -> thm -> string + val theory_long_name: thm -> string + val theory_base_name: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int val shyps_of: thm -> sort Ord_List.T @@ -494,7 +496,10 @@ val cert_of = #cert o rep_thm; val theory_id = Context.certificate_theory_id o cert_of; -val theory_name = Context.theory_id_name o theory_id; + +fun theory_name long = Context.theory_id_name long o theory_id; +val theory_long_name = theory_name {long = true}; +val theory_base_name = theory_name {long = false}; val maxidx_of = #maxidx o rep_thm; fun maxidx_thm th i = Int.max (maxidx_of th, i); @@ -2399,7 +2404,7 @@ val th' = th |> unconstrainT |> tap (expose_proof thy) |> trim_context; val prop = plain_prop_of th; val (t, Ss, c) = Logic.dest_arity prop; - val ar = ((t, Ss, c), (th', Context.theory_name thy, serial ())); + val ar = ((t, Ss, c), (th', Context.theory_base_name thy, serial ())); in thy |> Sign.primitive_arity (t, Ss, [c]) diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Tools/Code/code_runtime.ML Thu Apr 20 11:57:34 2023 +0200 @@ -718,7 +718,7 @@ val code_binding = Path.map_binding Code_Target.code_path binding; val preamble = "(* Generated from " ^ - Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^ + Path.implode (Resources.thy_path (Path.basic (Context.theory_base_name thy))) ^ "; DO NOT EDIT! *)"; val thy' = Code_Target.export code_binding (Bytes.string (preamble ^ "\n\n" ^ code)) thy; val _ = Code_Target.code_export_message thy'; diff -r 3c837f8c8ed5 -r 5db014c36f42 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Tools/Code/code_thingol.ML Thu Apr 20 11:57:34 2023 +0200 @@ -1009,7 +1009,7 @@ let val thy = Proof_Context.theory_of ctxt; fun this_theory name = - if Context.theory_name thy = name then thy + if Context.theory_base_name thy = name then thy else Context.get_theory {long = false} thy name; fun consts_of thy' =