# HG changeset patch
# User paulson
# Date 1220969828 -7200
# Node ID 6ab2cab482479461524aa8b295382dd8b6e6afca
# Parent  626f0a79a4b9248debffbd4d0a711d4e038b47d8
 Overall exception handler in order to insulate our users from low-level bugs.

diff -r 626f0a79a4b9 -r 6ab2cab48247 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Tue Sep 09 16:16:20 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Tue Sep 09 16:17:08 2008 +0200
@@ -590,7 +590,7 @@
     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*)
@@ -605,8 +605,9 @@
                   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;