1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jan 10 15:30:17 2011 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jan 10 15:45:46 2011 +0100
     1.3 @@ -399,10 +399,10 @@
     1.4        if exec then
     1.5          let
     1.6            val _ = Output.urgent_message ("BEFORE PARTITION OF " ^
     1.7 -                            Int.toString (length mutants) ^ " MUTANTS")
     1.8 +                            string_of_int (length mutants) ^ " MUTANTS")
     1.9            val (execs, noexecs) = List.partition (is_executable_term thy) (take_random (20 * max_mutants) mutants)
    1.10 -          val _ = tracing ("AFTER PARTITION (" ^ Int.toString (length execs) ^
    1.11 -                           " vs " ^ Int.toString (length noexecs) ^ ")")
    1.12 +          val _ = tracing ("AFTER PARTITION (" ^ string_of_int (length execs) ^
    1.13 +                           " vs " ^ string_of_int (length noexecs) ^ ")")
    1.14          in
    1.15            execs @ take_random (Int.max (0, max_mutants - length execs)) noexecs
    1.16          end
    1.17 @@ -468,10 +468,10 @@
    1.18  (* subentry -> string *)
    1.19  fun string_for_subentry (mtd_name, genuine_cex, potential_cex, no_cex, donno,
    1.20                           timeout, error) =
    1.21 -  "    " ^ mtd_name ^ ": " ^ Int.toString genuine_cex ^ "+ " ^
    1.22 -  Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^
    1.23 -  Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^
    1.24 -  Int.toString error ^ "!"
    1.25 +  "    " ^ mtd_name ^ ": " ^ string_of_int genuine_cex ^ "+ " ^
    1.26 +  string_of_int potential_cex ^ "= " ^ string_of_int no_cex ^ "- " ^
    1.27 +  string_of_int donno ^ "? " ^ string_of_int timeout ^ "T " ^
    1.28 +  string_of_int error ^ "!"
    1.29  
    1.30  (* entry -> string *)
    1.31  fun string_for_entry (thm_name, exec, subentries) =