diff -r 9267a04aabe6 -r 2f9877db82a1 src/HOL/Mirabelle/Tools/mirabelle_arith.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Thu May 13 15:52:10 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(*  Title:      HOL/Mirabelle/Tools/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 Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout")
-
-fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
-
-end