--- a/src/Pure/library.ML Mon Jan 10 16:45:28 2011 +0100+++ b/src/Pure/library.ML Mon Jan 10 16:56:47 2011 +0100@@ -644,7 +644,7 @@ local val zero = ord "0";- val small = 10000;+ val small = 10000: int; val small_table = Vector.tabulate (small, Int.toString); in