/*

Version 1.0 06/09/1995

Author: Sjaak Smetsers 

*/

extern void PrintNodeSymbol (Node node, int arg_nr, File file);