fprintf_filtered (stream, "type ");
fprintf_filtered (stream, "%s = ", SYMBOL_PRINT_NAME (new_symbol));
type_print (type, "", stream, 0);
fprintf_filtered (stream, "type ");
fprintf_filtered (stream, "%s = ", SYMBOL_PRINT_NAME (new_symbol));
type_print (type, "", stream, 0);