# HG changeset patch
# User wenzelm
# Date 1136672873 -3600
# Node ID 3618d5ae0ac8023c0081b886643f7940ffe6b2ae
# Parent  3cdfa57408be832ef9aebf80ad0fe93f6255b4e4
gen_names: preserve empty names;

diff -r 3cdfa57408be -r 3618d5ae0ac8 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Jan 07 23:27:52 2006 +0100
+++ b/src/Pure/pure_thy.ML	Sat Jan 07 23:27:53 2006 +0100
@@ -294,8 +294,8 @@
 
 (* naming *)
 
-fun gen_names j len name =
-  map (fn i => name ^ "_" ^ string_of_int i) (j + 1 upto j + len);
+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 xs = gen_names 0 (length xs) name ~~ xs;