# HG changeset patch
# User wenzelm
# Date 1566235458 -7200
# Node ID bf1a5901448107006378d165dd3644026f2063ae
# Parent  503ca64329cc7557a7f134456f90d3b7309aa522
tuned;

diff -r 503ca64329cc -r bf1a59014481 src/Pure/thm_name.ML
--- 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;