# HG changeset patch # User wenzelm # Date 1703417545 -3600 # Node ID 670b3dc1daeedc02b4fef693d149da7ee50bbdd0 # Parent 5ebb8e7a2847ea64270b94edb78477c4dca57564 clarified modules; diff -r 5ebb8e7a2847 -r 670b3dc1daee src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Sun Dec 24 12:23:50 2023 +0100 +++ b/src/Pure/Isar/generic_target.ML Sun Dec 24 12:32:25 2023 +0100 @@ -349,6 +349,8 @@ in (result'', result) end; +fun burrow_fact f = split_list #>> burrow f #> op ~~; + in fun notes target_notes kind facts lthy = @@ -356,7 +358,7 @@ val facts' = facts |> map (fn (a, thms) => let val name_pos = Local_Theory.bind_name lthy (fst a); - val thms' = Global_Theory.burrow_fact (Global_Theory.name_multi name_pos) thms; + val thms' = burrow_fact (Global_Theory.name_multi name_pos) thms; in (a, (map o apfst o map) (import_export_proof lthy) thms') end); val local_facts = Attrib.map_thms #1 facts'; val global_facts = Attrib.map_thms #2 facts'; diff -r 5ebb8e7a2847 -r 670b3dc1daee src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Sun Dec 24 12:23:50 2023 +0100 +++ b/src/Pure/global_theory.ML Sun Dec 24 12:32:25 2023 +0100 @@ -23,7 +23,6 @@ val transfer_theories: theory -> thm -> thm val all_thms_of: theory -> bool -> (string * thm) list val get_thm_name: theory -> Thm_Name.T * Position.T -> thm - val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list val register_proofs_lazy: string * Position.T -> thm list lazy -> theory -> thm list lazy * theory val register_proofs: string * Position.T -> thm list -> theory -> thm list * theory val name_multi: string * Position.T -> thm list -> ((string * Position.T) * thm) list @@ -206,11 +205,6 @@ (** store theorems **) -(* fact specifications *) - -fun burrow_fact f = split_list #>> burrow f #> op ~~; - - (* register proofs *) fun check_thms_lazy (thms: thm list lazy) =