# HG changeset patch
# User wenzelm
# Date 1206658978 -3600
# Node ID 9385d441cec67fbf6abd2658845292b375155240
# Parent  a63501938ce18b046b02a6154fa6d7eeff3990b0
tuned;

diff -r a63501938ce1 -r 9385d441cec6 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Mar 28 00:02:56 2008 +0100
+++ b/src/Pure/pure_thy.ML	Fri Mar 28 00:02:58 2008 +0100
@@ -236,11 +236,9 @@
 
 (* naming *)
 
-fun gen_names _ len "" = replicate len ""
-  | gen_names j len name = map (fn i => name ^ "_" ^ string_of_int i) (j + 1 upto j + len);
-
 fun name_multi name [x] = [(name, x)]
-  | name_multi name xs = gen_names 0 (length xs) name ~~ xs;
+  | name_multi "" xs = map (pair "") xs
+  | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
 
 fun name_thm pre official name thm = thm
   |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)