diff -r 44d1f4e0a46e -r 15f4309bb9eb src/HOL/Mirabelle/Tools/mirabelle_arith.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Tue Apr 24 13:59:29 2012 +0100
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Mirabelle/Actions/mirabelle_arith.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
+*)
+
+structure Mirabelle_Arith : MIRABELLE_ACTION =
+struct
+
+fun arith_tag id = "#" ^ string_of_int id ^ " arith: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
+  if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
+  then log (arith_tag id ^ "succeeded")
+  else ()
+  handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
+
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
+
+end