src/Pure/facts.ML

   val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   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;
 
 structure Facts: FACTS =
 struct

 (** get individual theorems **)
 
 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
     fun print_name () =
       markup_extern (Context.proof_of context) facts name |-> Markup.markup;