1.1 --- a/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 15:30:05 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 15:47:39 2009 +0200
     1.3 @@ -1,2 +1,3 @@
     1.4 -if can (unprefix "polyml") (getenv "ML_SYSTEM") then use_thy "MirabelleTest"
     1.5 +if String.isPrefix "polyml" ml_system
     1.6 +then use_thy "MirabelleTest"
     1.7  else ();

     2.1 --- a/src/HOL/Mirabelle/lib/scripts/report.pl	Thu Sep 03 15:30:05 2009 +0200
     2.2 +++ b/src/HOL/Mirabelle/lib/scripts/report.pl	Thu Sep 03 15:47:39 2009 +0200
     2.3 @@ -59,8 +59,8 @@
     2.4    print FILE "Total number of sledgehammer calls: $sh_calls\n";
     2.5    print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
     2.6    printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
     2.7 -  print FILE "Total time for successful sledgehammer calls: $time seconds\n";
     2.8 -  print FILE "Average time for successful sledgehammer calls: $avg_time seconds\n\n";
     2.9 +  printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time;
    2.10 +  printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time;
    2.11  }
    2.12  
    2.13  if ($metis_calls > 0) {
    2.14 @@ -71,8 +71,8 @@
    2.15    print FILE "Number of successful metis calls: $metis_succeeded\n";
    2.16    print FILE "Number of metis time outs: $metis_time_out\n";
    2.17    printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent;
    2.18 -  print FILE "Total time for successful metis calls: $time seconds\n";
    2.19 -  print FILE "Average time for successful metis calls: $avg_time seconds\n";
    2.20 +  printf FILE "Total time for successful metis calls: %.3f seconds\n", $time;
    2.21 +  printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time;
    2.22  }
    2.23  
    2.24  close(FILE);