src/HOL/Tools/metis_tools.ML

                 else Output.debug (fn () => "goal is higher-order")
         val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
     in
         case refute thms of
             Metis.Resolution.Contradiction mth =>
-              let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
+             (let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
                             Metis.Thm.toString mth)
                   val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
                                (*add constraints arising from converting goal to clause form*)
                   val proof = Metis.Proof.proof mth
                   val result = translate isFO ctxt' axioms proof

               in
                   if null unused then ()
                   else warning ("Unused theorems: " ^ commas (map #1 unused));
                   case result of
                       (_,ith)::_ => (Output.debug (fn () => "success: " ^ Display.string_of_thm ith); ith)
-                    | _ => error "METIS: no result"
+                    | _ => error "Metis: no result"
               end
+              handle e => error "Metis: Exception raised during proof reconstruction")
           | Metis.Resolution.Satisfiable _ => error "Metis: No first-order proof with the lemmas supplied"
     end;
 
   fun metis_general_tac mode ctxt ths i st0 =
     let val _ = Output.debug (fn () =>