# HG changeset patch
# User wenzelm
# Date 1254512551 -7200
# Node ID 51fda1c8fa2df55bde5c5683ecefc201d5cc8995
# Parent  394d37f19e0a7f535a2a4a9abcc085a989ac1e94
Refute.refute_goal: goal addressing from 1 as usual;

diff -r 394d37f19e0a -r 51fda1c8fa2d src/HOL/Mirabelle/Tools/mirabelle_refute.ML
--- 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"))