# HG changeset patch
# User blanchet
# Date 1280427350 -7200
# Node ID 5e4ad2df09f339a74f9c59b0037141ef69000cc2
# Parent  488b38cd3e0627641492d4b66b15bd46f5573bfb
revert exception throwing in FOL_SOLVE, since they're not caught anyway

diff -r 488b38cd3e06 -r 5e4ad2df09f3 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 29 20:02:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 29 20:15:50 2010 +0200
@@ -764,12 +764,11 @@
                     (_,ith)::_ =>
                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
                          [ith])
-                  | _ => (trace_msg (fn () => "Metis: No result");
-                          raise METIS ("FOL_SOLVE", ""))
+                  | _ => (trace_msg (fn () => "Metis: No result"); [])
             end
         | Metis.Resolution.Satisfiable _ =>
             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
-             raise METIS ("FOL_SOLVE", ""))
+             [])
   end;
 
 val type_has_top_sort =