src/HOL/Mirabelle/Tools/mirabelle_refute.ML
changeset 32858 51fda1c8fa2d
parent 32564 378528d2f7eb
child 35593 88b49baba092
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Oct 02 21:41:57 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Fri Oct 02 21:42:31 2009 +0200
@@ -9,11 +9,11 @@
 (* FIXME:
 fun refute_action args timeout {pre=st, ...} = 
   let
-    val subgoal = 0
+    val subgoal = 1
     val thy     = Proof.theory_of st
     val thm = goal_thm_of st
 
-    val refute = Refute.refute_subgoal thy args thm
+    val refute = Refute.refute_goal thy args thm
     val _ = TimeLimit.timeLimit timeout refute subgoal
   in
     val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))