1(*  Title:      Pure/thm_name.ML
2    Author:     Makarius
3
4Systematic naming of individual theorems, as selections from multi-facts.
5
6  (NAME, 0): the single entry of a singleton fact NAME
7  (NAME, i): entry i of a non-singleton fact (1 <= i <= length)
8*)
9
10signature THM_NAME =
11sig
12  type T = string * int
13  val ord: T ord
14  val print: T -> string
15  val flatten: T -> string
16  val make_list: string -> thm list -> (T * thm) list
17end;
18
19structure Thm_Name: THM_NAME =
20struct
21
22type T = string * int;
23val ord = prod_ord string_ord int_ord;
24
25fun print (name, index) =
26  if name = "" orelse index = 0 then name
27  else name ^ enclose "(" ")" (string_of_int index);
28
29fun flatten (name, index) =
30  if name = "" orelse index = 0 then name
31  else name ^ "_" ^ string_of_int index;
32
33fun make_list name [thm: thm] = [((name, 0), thm)]
34  | make_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
35
36end;
37