src/HOL/Mirabelle/Tools/mirabelle.ML

   let
     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
+      SOME _ => true
     | NONE => false)
   end
 
 local