# HG changeset patch
# User boehmes
# Date 1250853833 -7200
# Node ID 18bbd9f4c2cdc1bef9153fa179b32f3cf99ee223
# Parent  594890623c466d946d1b1946ca98f27c7e5b369b
disabled refute action (needs changes in the code of refute)

diff -r 594890623c46 -r 18bbd9f4c2cd src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML
--- 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