printf ("<dimension index=\"%d\">\n", indx);
dump_value (stdout, 0, false);
printf ("<dimension index=\"%d\">\n", indx);
dump_value (stdout, 0, false);
dump_value(stdout, 1, false);
fprintf (stdout, " </datum>\n");
}
dump_value(stdout, 1, false);
fprintf (stdout, " </datum>\n");
}