diff --git a/src/HOL/Mirabelle/Mirabelle_Test.thy b/src/HOL/Mirabelle/Mirabelle_Test.thy
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy
@@ -1,24 +1,23 @@
 (*  Title:      HOL/Mirabelle/Mirabelle_Test.thy
     Author:     Sascha Boehme, TU Munich
 *)
 
 section \<open>Simple test theory for Mirabelle actions\<close>
 
 theory Mirabelle_Test
 imports Main Mirabelle
 begin
 
 ML_file \<open>Tools/mirabelle_arith.ML\<close>
 ML_file \<open>Tools/mirabelle_metis.ML\<close>
 ML_file \<open>Tools/mirabelle_quickcheck.ML\<close>
-ML_file \<open>Tools/mirabelle_refute.ML\<close>
 ML_file \<open>Tools/mirabelle_sledgehammer.ML\<close>
 ML_file \<open>Tools/mirabelle_sledgehammer_filter.ML\<close>
 ML_file \<open>Tools/mirabelle_try0.ML\<close>
 
 text \<open>
   Only perform type-checking of the actions,
   any reasonable test would be too complicated.
 \<close>
 
 end
diff --git a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML
deleted file mode 100644
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML
+++ /dev/null
@@ -1,39 +0,0 @@
-(*  Title:      HOL/Mirabelle/Tools/mirabelle_refute.ML
-    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
-*)
-
-structure Mirabelle_Refute : MIRABELLE_ACTION =
-struct
-
-
-(* FIXME:
-fun refute_action args timeout {pre=st, ...} = 
-  let
-    val subgoal = 1
-    val thy = Proof.theory_of st
-    val thm = #goal (Proof.raw_goal st)
-
-    val refute = Refute.refute_goal thy args thm
-    val _ = Timeout.apply timeout refute subgoal
-  in
-    val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
-    val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
-
-    val r =
-      if Substring.isSubstring "model found" writ_log
-      then
-        if Substring.isSubstring "spurious" warn_log
-        then SOME "potential counterexample"
-        else SOME "real counterexample (bug?)"
-      else
-        if Substring.isSubstring "time limit" writ_log
-        then SOME "no counterexample (timeout)"
-        else if Substring.isSubstring "Search terminated" writ_log
-        then SOME "no counterexample (normal termination)"
-        else SOME "no counterexample (unknown)"
-  in r end
-*)
-
-fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
-
-end