# HG changeset patch
# User wenzelm
# Date 1565956911 -7200
# Node ID 8bc7e54bead925372cf4811cdc62e896211bce03
# Parent  2970fdc230cc2d292dbe2fad94df4df019103b4b
clarified signature;

diff -r 2970fdc230cc -r 8bc7e54bead9 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Fri Aug 16 11:40:13 2019 +0200
+++ b/src/Pure/facts.ML	Fri Aug 16 14:01:51 2019 +0200
@@ -46,7 +46,8 @@
   val hide: bool -> string -> T -> T
   type thm_name = string * int
   val thm_name_ord: thm_name * thm_name -> order
-  val single_thm_name: string -> thm_name
+  val thm_name_flat: thm_name -> string
+  val thm_name_list: string -> thm list -> (thm_name * thm) list
   val get_thm: Context.generic -> T -> thm_name * Position.T -> thm
 end;
 
@@ -305,7 +306,12 @@
 type thm_name = string * int;
 val thm_name_ord = prod_ord string_ord int_ord;
 
-fun single_thm_name name : thm_name = (name, 0);
+fun thm_name_flat (name, i) =
+  if name = "" orelse i = 0 then name
+  else name ^ "_" ^ string_of_int i;
+
+fun thm_name_list name [thm: thm] = [((name, 0), thm)]
+  | thm_name_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
 
 fun get_thm context facts ((name, i), pos) =
   let
diff -r 2970fdc230cc -r 8bc7e54bead9 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Aug 16 11:40:13 2019 +0200
+++ b/src/Pure/global_theory.ML	Fri Aug 16 14:01:51 2019 +0200
@@ -19,7 +19,7 @@
   val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
   val burrow_facts: ('a list -> 'b list) ->
     ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
-  val name_multi: string * Position.T -> 'a list -> ((string * Position.T) * 'a) list
+  val name_multi: string * Position.T -> thm list -> ((string * Position.T) * thm) list
   type name_flags
   val unnamed: name_flags
   val official1: name_flags
@@ -134,15 +134,11 @@
 
 end;
 
-fun name_multi (name, pos: Position.T) xs =
-  (case xs of
-    [x] => [((name, pos), x)]
-  | _ =>
-      if name = "" then map (pair ("", pos)) xs
-      else map_index (fn (i, x) => ((name ^ "_" ^ string_of_int (i + 1), pos), x)) xs);
+fun name_multi (name, pos) =
+  Facts.thm_name_list name #> (map o apfst) (fn thm_name => (Facts.thm_name_flat thm_name, pos));
 
-fun name_thms name_flags name_pos thms =
-  map (uncurry (name_thm name_flags)) (name_multi name_pos thms);
+fun name_thms name_flags name_pos =
+  name_multi name_pos #> map (uncurry (name_thm name_flags));
 
 
 (* apply theorems and attributes *)