diff -r 9e14fbd43e6b -r 372d6749f00e src/Tools/Metis/src/Parser.sml
--- a/src/Tools/Metis/src/Parser.sml	Tue Nov 13 17:04:16 2007 +0100
+++ b/src/Tools/Metis/src/Parser.sml	Tue Nov 13 18:29:28 2007 +0100
@@ -129,6 +129,7 @@
 
 fun ppTriple ppA ppB ppC = ppBracket "(" ")" (ppTrinop "," "," ppA ppB ppC);
 
+(* Keep eta expanded to evaluate lineLength when supplied with a *)
 fun toString ppA a = PP.pp_to_string (!lineLength) ppA a;
 
 fun fromString toS = ppMap toS ppString;