revert exception throwing in FOL_SOLVE, since they're not caught anyway

--- 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 =