changeset 35593 | 88b49baba092 |
parent 32858 | 51fda1c8fa2d |
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Mar 05 23:51:32 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Mar 05 23:52:09 2010 +0100 @@ -10,8 +10,8 @@ fun refute_action args timeout {pre=st, ...} = let val subgoal = 1 - val thy = Proof.theory_of st - val thm = goal_thm_of st + val thy = Proof.theory_of st + val thm = #goal (Proof.raw_goal st) val refute = Refute.refute_goal thy args thm val _ = TimeLimit.timeLimit timeout refute subgoal