1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 11 21:43:19 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -252,10 +252,6 @@
     1.4    Other characters go to _nnn where nnn is the decimal ASCII code.*)
     1.5  val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
     1.6  
     1.7 -fun stringN_of_int 0 _ = ""
     1.8 -  | stringN_of_int k n =
     1.9 -    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
    1.10 -
    1.11  fun ascii_of_char c =
    1.12    if Char.isAlphaNum c then
    1.13      String.str c