1.1 --- a/src/Pure/pure_thy.ML	Fri Mar 28 00:02:56 2008 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Fri Mar 28 00:02:58 2008 +0100
     1.3 @@ -236,11 +236,9 @@
     1.4  
     1.5  (* naming *)
     1.6  
     1.7 -fun gen_names _ len "" = replicate len ""
     1.8 -  | gen_names j len name = map (fn i => name ^ "_" ^ string_of_int i) (j + 1 upto j + len);
     1.9 -
    1.10  fun name_multi name [x] = [(name, x)]
    1.11 -  | name_multi name xs = gen_names 0 (length xs) name ~~ xs;
    1.12 +  | name_multi "" xs = map (pair "") xs
    1.13 +  | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
    1.14  
    1.15  fun name_thm pre official name thm = thm
    1.16    |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)