--- a/src/Pure/thm_name.ML Mon Aug 19 19:12:44 2019 +0200
+++ b/src/Pure/thm_name.ML Mon Aug 19 19:24:18 2019 +0200
@@ -22,13 +22,13 @@
type T = string * int;
val ord = prod_ord string_ord int_ord;
-fun print (name, i) =
- if name = "" orelse i = 0 then name
- else name ^ enclose "(" ")" (string_of_int i);
+fun print (name, index) =
+ if name = "" orelse index = 0 then name
+ else name ^ enclose "(" ")" (string_of_int index);
-fun flatten (name, i) =
- if name = "" orelse i = 0 then name
- else name ^ "_" ^ string_of_int i;
+fun flatten (name, index) =
+ if name = "" orelse index = 0 then name
+ else name ^ "_" ^ string_of_int index;
fun make_list name [thm: thm] = [((name, 0), thm)]
| make_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;