# 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) =