--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Sat Sep 05 11:45:57 2009 +0200
@@ -5,12 +5,17 @@
structure Mirabelle_Arith : MIRABELLE_ACTION =
struct
-fun arith_action {pre, timeout, log, ...} =
+fun arith_tag id = "#" ^ string_of_int id ^ " arith: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id {pre, timeout, log, ...} =
if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
- then log "arith: succeeded"
+ then log (arith_tag id ^ "succeeded")
else ()
- handle TimeLimit.TimeOut => log "arith: timeout"
+ handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
-fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action)
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
end