# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 01ef1c3d9cfd7f86afa038fcd8c316e1ad8d03a5
# Parent  86683865278d9decfb8e6bea2ca8d9673923d80b
more robust exception handling in Metis (also works if there are several subgoals)

diff -r 86683865278d -r 01ef1c3d9cfd src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
@@ -122,7 +122,15 @@
              else
                ();
              [])
-  end;
+  end
+  handle METIS (loc, msg) =>
+         if mode <> FT then
+           (verbose_warning ctxt ("Falling back on \"metisFT\".");
+            FOL_SOLVE FT ctxt cls ths0)
+         else
+           error ("Failed to replay Metis proof in Isabelle." ^
+                  (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
+                   else ""))
 
 (* Extensionalize "th", because that makes sense and that's what Sledgehammer
    does, but also keep an unextensionalized version of "th" for backward
@@ -163,15 +171,6 @@
       Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
-      handle METIS (loc, msg) =>
-             if mode <> FT then
-               (verbose_warning ctxt ("Falling back on \"metisFT\".");
-                generic_metis_tac FT ctxt ths i st0)
-             else
-               error ("Failed to replay Metis proof in Isabelle." ^
-                      (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
-                       else ""))
-
   end
 
 val metis_tac = generic_metis_tac HO