# HG changeset patch
# User boehmes
# Date 1251985659 -7200
# Node ID 9da37876874db290f5da2c01ee339a4557d3fe0c
# Parent  212530b16e6eebd494f5a7f6f8c19414ce352e0e
tuned

diff -r 212530b16e6e -r 9da37876874d src/HOL/Mirabelle/ROOT.ML
--- a/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 15:30:05 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 15:47:39 2009 +0200
@@ -1,2 +1,3 @@
-if can (unprefix "polyml") (getenv "ML_SYSTEM") then use_thy "MirabelleTest"
+if String.isPrefix "polyml" ml_system
+then use_thy "MirabelleTest"
 else ();
diff -r 212530b16e6e -r 9da37876874d src/HOL/Mirabelle/lib/scripts/report.pl
--- a/src/HOL/Mirabelle/lib/scripts/report.pl	Thu Sep 03 15:30:05 2009 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/report.pl	Thu Sep 03 15:47:39 2009 +0200
@@ -59,8 +59,8 @@
   print FILE "Total number of sledgehammer calls: $sh_calls\n";
   print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
   printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
-  print FILE "Total time for successful sledgehammer calls: $time seconds\n";
-  print FILE "Average time for successful sledgehammer calls: $avg_time seconds\n\n";
+  printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time;
+  printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time;
 }
 
 if ($metis_calls > 0) {
@@ -71,8 +71,8 @@
   print FILE "Number of successful metis calls: $metis_succeeded\n";
   print FILE "Number of metis time outs: $metis_time_out\n";
   printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent;
-  print FILE "Total time for successful metis calls: $time seconds\n";
-  print FILE "Average time for successful metis calls: $avg_time seconds\n";
+  printf FILE "Total time for successful metis calls: %.3f seconds\n", $time;
+  printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time;
 }
 
 close(FILE);