# HG changeset patch
# User wenzelm
# Date 1703689062 -3600
# Node ID d02c8adce4e6db0ffb35ef64527df70420d0b5b9
# Parent  a2fbac74fba7c089e598739948a9f4963dea8cc1
clarified modules;

diff -r a2fbac74fba7 -r d02c8adce4e6 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Dec 27 15:50:17 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Wed Dec 27 15:57:42 2023 +0100
@@ -296,8 +296,6 @@
 
 local
 
-fun name_thms name = split_list #>> burrow (Thm_Name.list name) #> op ~~;
-
 val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.flatten;
 val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.flatten;
 
@@ -366,7 +364,7 @@
     val (facts', lthy') =
       (facts, lthy) |-> fold_map (fn (a, thms) => fn lthy1 =>
         let
-          val thms1 = name_thms (Local_Theory.full_name_pos lthy1 (fst a)) thms;
+          val thms1 = Thm_Name.expr (Local_Theory.full_name_pos lthy1 (fst a)) thms;
           val (thms2, lthy2) =
             (thms1, lthy1) |-> fold_map (fn (args, atts) =>
               fold_map thm_definition args #>> rpair atts);
diff -r a2fbac74fba7 -r d02c8adce4e6 src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Wed Dec 27 15:50:17 2023 +0100
+++ b/src/Pure/thm_name.ML	Wed Dec 27 15:57:42 2023 +0100
@@ -14,6 +14,7 @@
   val print: T -> string
   val flatten: T * Position.T -> string * Position.T
   val list: string * Position.T -> 'a list -> ((T * Position.T) * 'a) list
+  val expr: string * Position.T -> ('a list * 'b) list -> (((T * Position.T) * 'a) list * 'b) list
 end;
 
 structure Thm_Name: THM_NAME =
@@ -33,4 +34,6 @@
 fun list (name, pos: Position.T) [thm] = [(((name, 0): T, pos), thm)]
   | list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
 
+fun expr name = split_list #>> burrow (list name) #> op ~~;
+
 end;