# HG changeset patch
# User wenzelm
# Date 1620832666 -7200
# Node ID 8c4ba5f612234e9e05583f4dfb2579dcb1a28caa
# Parent  54fe8cc0e1c659dc9268ddf19ad5cd0457c71735
unused (see 8ffc607c345d);

diff -r 54fe8cc0e1c6 -r 8c4ba5f61223 src/HOL/Mirabelle/Mirabelle_Test.thy
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Wed May 12 16:47:52 2021 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Wed May 12 17:17:46 2021 +0200
@@ -11,7 +11,6 @@
 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>
diff -r 54fe8cc0e1c6 -r 8c4ba5f61223 src/HOL/Mirabelle/Tools/mirabelle_refute.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Wed May 12 16:47:52 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -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