src/Pure/library.ML
changeset 41494 364f672d8827
parent 41492 7a4138cb46db
child 41516 3a70387b5e01
     1.1 --- a/src/Pure/library.ML	Mon Jan 10 16:45:28 2011 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Jan 10 16:56:47 2011 +0100
     1.3 @@ -644,7 +644,7 @@
     1.4  
     1.5  local
     1.6    val zero = ord "0";
     1.7 -  val small = 10000;
     1.8 +  val small = 10000: int;
     1.9    val small_table = Vector.tabulate (small, Int.toString);
    1.10  in
    1.11