diff -r 9e91959a8cfc -r ebd5366e7a42 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Mar 24 16:19:54 2013 +0100
+++ b/src/Pure/General/pretty.scala	Mon Mar 25 10:37:38 2013 +0100
@@ -31,14 +31,12 @@
   abstract class Metric
   {
     val unit: Double
-    def average: Double
     def apply(s: String): Double
   }
 
   object Metric_Default extends Metric
   {
     val unit = 1.0
-    val average = 1.0
     def apply(s: String): Double = s.length.toDouble
   }