tuned

--- a/src/HOL/IsaMakefile	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri Sep 04 13:57:56 2009 +0200
@@ -1124,7 +1124,7 @@
 
 HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
 
-$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/MirabelleTest.thy \
+$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \
   Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
   Mirabelle/Tools/mirabelle_arith.ML \
   Mirabelle/Tools/mirabelle_metis.ML \

--- a/src/HOL/Mirabelle/MirabelleTest.thy	Fri Sep 04 10:58:50 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: MirabelleTest.thy
-   Author: Sascha Boehme
-*)
-
-header {* Simple test theory for Mirabelle actions *}
-
-theory MirabelleTest
-imports Main Mirabelle
-uses
-  "Tools/mirabelle_arith.ML"
-  "Tools/mirabelle_metis.ML"
-  "Tools/mirabelle_quickcheck.ML"
-  "Tools/mirabelle_refute.ML"
-  "Tools/mirabelle_sledgehammer.ML"
-begin
-
-(*
-  only perform type-checking of the actions,
-  any reasonable test would be too complicated
-*)
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Fri Sep 04 13:57:56 2009 +0200
@@ -0,0 +1,22 @@
+(* Title: Mirabelle_Test.thy
+   Author: Sascha Boehme
+*)
+
+header {* Simple test theory for Mirabelle actions *}
+
+theory Mirabelle_Test
+imports Main Mirabelle
+uses
+  "Tools/mirabelle_arith.ML"
+  "Tools/mirabelle_metis.ML"
+  "Tools/mirabelle_quickcheck.ML"
+  "Tools/mirabelle_refute.ML"
+  "Tools/mirabelle_sledgehammer.ML"
+begin
+
+(*
+  only perform type-checking of the actions,
+  any reasonable test would be too complicated
+*)
+
+end

--- a/src/HOL/Mirabelle/ROOT.ML	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML	Fri Sep 04 13:57:56 2009 +0200
@@ -1,1 +1,1 @@
-use_thy "MirabelleTest";
+use_thy "Mirabelle_Test";

--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Fri Sep 04 13:57:56 2009 +0200
@@ -9,7 +9,7 @@
   if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
   then log "arith: succeeded"
   else ()
-  handle TimeLimit.TimeOut => log "arith: time out"
+  handle TimeLimit.TimeOut => log "arith: timeout"
 
 fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action)
 

--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 04 13:57:56 2009 +0200
@@ -20,7 +20,7 @@
     |> add_info
     |> log
   end
-  handle TimeLimit.TimeOut => log "metis: time out"
+  handle TimeLimit.TimeOut => log "metis: timeout"
 
 fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action)
 

--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Sep 04 13:57:56 2009 +0200
@@ -14,7 +14,7 @@
       NONE => log "quickcheck: no counterexample"
     | SOME _ => log "quickcheck: counterexample found")
   end
-  handle TimeLimit.TimeOut => log "quickcheck: time out"
+  handle TimeLimit.TimeOut => log "quickcheck: timeout"
 
 fun invoke args =
   Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args))

--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Sep 04 13:57:56 2009 +0200
@@ -27,7 +27,7 @@
         else SOME "real counterexample (bug?)"
       else
         if Substring.isSubstring "time limit" writ_log
-        then SOME "no counterexample (time out)"
+        then SOME "no counterexample (timeout)"
         else if Substring.isSubstring "Search terminated" writ_log
         then SOME "no counterexample (normal termination)"
         else SOME "no counterexample (unknown)"

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 04 13:57:56 2009 +0200
@@ -55,7 +55,7 @@
       TimeLimit.timeLimit timeout atp (Proof.get_goal st)
   in if success then (message, SOME (time, thm_names)) else (message, NONE) end
   handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
-       | TimeLimit.TimeOut => ("time out", NONE)
+       | TimeLimit.TimeOut => ("timeout", NONE)
        | ERROR msg => ("error: " ^ msg, NONE)
 
 in
@@ -87,7 +87,7 @@
     fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
     fun timed_metis thms =
       uncurry with_time (Mirabelle.cpu_time apply_metis thms)
-      handle TimeLimit.TimeOut => "time out"
+      handle TimeLimit.TimeOut => "timeout"
            | ERROR msg => "error: " ^ msg
     fun log_metis s = log (metis_tag ^ s)
   in

--- a/src/HOL/Mirabelle/lib/scripts/report.pl	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/report.pl	Fri Sep 04 13:57:56 2009 +0200
@@ -39,7 +39,7 @@
     $metis_succeeded++;
     $metis_time += $1;
   }
-  if (m/^metis \(sledgehammer\): time out/) {
+  if (m/^metis \(sledgehammer\): timeout/) {
     $metis_timeout++;
   }
 }