src/Pure/General/ml_syntax.ML
Mon, 16 Apr 2007 12:16:11 +0200 wenzelm added print_indexname;
less more (0) -1 tip