use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Mar 05 23:31:58 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Mar 05 23:51:32 2010 +0100
@@ -27,7 +27,6 @@
     unit
 
   (*utility functions*)
-  val goal_thm_of : Proof.state -> thm
   val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
     Proof.state -> bool
   val theorems_in_proof_term : thm -> thm list
@@ -155,11 +154,9 @@
 
 (* Mirabelle utility functions *)
 
-val goal_thm_of = #goal o Proof.raw_goal  (* FIXME ?? *)
-
 fun can_apply time tac st =
   let
-    val {context = ctxt, facts, goal} = Proof.raw_goal st   (* FIXME ?? *)
+    val {context = ctxt, facts, goal} = Proof.goal st
     val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
   in
     (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
@@ -201,7 +198,7 @@
     NONE => []
   | SOME st =>
       if not (Toplevel.is_proof st) then []
-      else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
+      else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st))))
 
 fun get_setting settings (key, default) =
   the_default default (AList.lookup (op =) settings key)

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 05 23:31:58 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 05 23:51:32 2010 +0100
@@ -307,7 +307,7 @@
 
 fun run_sh prover hard_timeout timeout dir st =
   let
-    val {context = ctxt, facts, goal} = Proof.raw_goal st   (* FIXME ?? *)
+    val {context = ctxt, facts, goal} = Proof.goal st
     val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
     val ctxt' =
       ctxt
@@ -434,39 +434,39 @@
   end
 
 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
-  let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre))  (* FIXME ?? *) in
-  if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
-  then () else
-  let
-    val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
-    val minimize = AList.defined (op =) args minimizeK
-    val metis_ft = AList.defined (op =) args metis_ftK
-
-    fun apply_metis m1 m2 =
-      if metis_ft
-      then
-        if not (Mirabelle.catch_result metis_tag false
-            (run_metis false m1 name (these (!named_thms))) id st)
+  let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
+    if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
+    then () else
+    let
+      val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
+      val minimize = AList.defined (op =) args minimizeK
+      val metis_ft = AList.defined (op =) args metis_ftK
+  
+      fun apply_metis m1 m2 =
+        if metis_ft
         then
+          if not (Mirabelle.catch_result metis_tag false
+              (run_metis false m1 name (these (!named_thms))) id st)
+          then
+            (Mirabelle.catch_result metis_tag false
+              (run_metis true m2 name (these (!named_thms))) id st; ())
+          else ()
+        else
           (Mirabelle.catch_result metis_tag false
-            (run_metis true m2 name (these (!named_thms))) id st; ())
-        else ()
-      else
-        (Mirabelle.catch_result metis_tag false
-          (run_metis false m1 name (these (!named_thms))) id st; ())
-  in 
-    change_data id (set_mini minimize);
-    Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
-    if is_some (!named_thms)
-    then
-     (apply_metis Unminimized UnminimizedFT;
-      if minimize andalso not (null (these (!named_thms)))
+            (run_metis false m1 name (these (!named_thms))) id st; ())
+    in 
+      change_data id (set_mini minimize);
+      Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
+      if is_some (!named_thms)
       then
-       (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
-        apply_metis Minimized MinimizedFT)
-      else ())
-    else ()
-  end
+       (apply_metis Unminimized UnminimizedFT;
+        if minimize andalso not (null (these (!named_thms)))
+        then
+         (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
+          apply_metis Minimized MinimizedFT)
+        else ())
+      else ()
+    end
   end
 
 fun invoke args =

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 05 23:31:58 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 05 23:51:32 2010 +0100
@@ -253,7 +253,7 @@
     NONE => warning ("Unknown external prover: " ^ quote name)
   | SOME prover =>
       let
-        val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *)
+        val {context = ctxt, facts, goal} = Proof.goal proof_state;
         val desc =
           "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Mar 05 23:31:58 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Mar 05 23:51:32 2010 +0100
@@ -117,7 +117,7 @@
     val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
-    val {context = ctxt, facts, goal} = Proof.raw_goal state   (* FIXME ?? *)
+    val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
      {with_full_types = ! ATP_Manager.full_types,
       subgoal = subgoalno,