# HG changeset patch
# User blanchet
# Date 1357203399 -3600
# Node ID df8ae0590be22062e662b6e5f7b34b4dd9a230b2
# Parent  2fac44deb8b515f4caaa76984b50058166e8ded6
avoid repeated calls to metis from "resolve_tac" in case of ultimate failure

diff -r 2fac44deb8b5 -r df8ae0590be2 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 03 00:02:15 2013 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 03 09:56:39 2013 +0100
@@ -218,13 +218,10 @@
                   | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
             end
         | Metis_Resolution.Satisfiable _ =>
-            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
-             if null fallback_type_encs then
-               ()
-             else
-               raise METIS ("FOL_SOLVE",
-                            "No first-order proof with the lemmas supplied");
-             [])
+            (trace_msg ctxt (fn () =>
+               "Metis: No first-order proof with the lemmas supplied");
+             raise METIS ("FOL_SOLVE",
+                          "No first-order proof with the lemmas supplied"))
   end
   handle METIS (loc, msg) =>
          case fallback_type_encs of