2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 (* internal functions *******************************************************)
17 let token, mode = n in
18 let n = token ^ "_", mode in
19 if List.mem n ns then rename ns n else n
21 let alpha_name acc attr =
26 let n = rename ns n in
27 n :: ns, E.Name n :: a
32 (* interface functions ******************************************************)
36 let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in
37 List.rev_append a names