1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sat Apr 14 23:34:18 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,21 +0,0 @@
     1.4 -(*  Title:      HOL/Mirabelle/Tools/mirabelle_arith.ML
     1.5 -    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     1.6 -*)
     1.7 -
     1.8 -structure Mirabelle_Arith : MIRABELLE_ACTION =
     1.9 -struct
    1.10 -
    1.11 -fun arith_tag id = "#" ^ string_of_int id ^ " arith: "
    1.12 -
    1.13 -fun init _ = I
    1.14 -fun done _ _ = ()
    1.15 -
    1.16 -fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
    1.17 -  if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
    1.18 -  then log (arith_tag id ^ "succeeded")
    1.19 -  else ()
    1.20 -  handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
    1.21 -
    1.22 -fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
    1.23 -
    1.24 -end