--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Fri Aug 21 13:21:19 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Fri Aug 21 13:23:53 2009 +0200
@@ -6,6 +6,7 @@
struct
+(* FIXME:
fun refute_action args {pre=st, ...} =
let
val subgoal = 0
@@ -30,7 +31,8 @@
then SOME "no counterexample (normal termination)"
else SOME "no counterexample (unknown)"
in r end
+*)
-fun invoke args = Mirabelle.register ("refute", refute_action args)
+fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*)
end