The toolid is necessary to make sure that tools are always
correctly sorted; there should not be two tools with the
same id in the same section.