diff -r 0f1e411a1448 -r a2ad5b824051 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jan 10 15:30:17 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jan 10 15:45:46 2011 +0100
@@ -97,7 +97,7 @@
   \% " ^ timestamp () ^ "\n" ::
   maps (fn (_, []) => []
          | (heading, lines) =>
-           "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
+           "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
            map (string_for_problem_line use_conjecture_for_hypotheses) lines)
        problem
 
@@ -138,7 +138,7 @@
         fun add j =
           let
             val nice_name = nice_prefix ^
-                            (if j = 0 then "" else "_" ^ Int.toString j)
+                            (if j = 0 then "" else "_" ^ string_of_int j)
           in
             case Symtab.lookup (snd the_pool) nice_name of
               SOME full_name' =>