gen_names: preserve empty names;

--- 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;