--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Oct 28 22:04:57 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Oct 28 22:18:00 2009 +0100
@@ -151,11 +151,11 @@
(* Mirabelle utility functions *)
-val goal_thm_of = snd o snd o Proof.get_goal
+val goal_thm_of = #goal o Proof.raw_goal (* FIXME ?? *)
fun can_apply time tac st =
let
- val (ctxt, (facts, goal)) = Proof.get_goal st
+ val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *)
val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
in
(case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of