src/HOL/Mirabelle/Tools/mirabelle.ML

   val register : action -> theory -> theory
   val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
     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
   val theorems_of_sucessful_proof : Toplevel.state option -> thm list
   val get_setting : (string * string) list -> string * string -> string

 
 
 
 (* 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
       SOME (thm, _) => true
     | NONE => false)

 fun theorems_of_sucessful_proof state =
   (case state of
     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)
 
 fun get_int_setting settings (key, default) =