# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 007117fed1831c025f331dafacd87d466ee262db
# Parent  acfc370df64b06d0fd61e5cb00825db5f657aee1
fall back in case path finder fails -- these errors are sometimes salvageable

diff -r acfc370df64b -r 007117fed183 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -516,13 +516,12 @@
       fun replace_item_list lx 0 (_::ls) = lx::ls
         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
       fun path_finder_fail tm ps t =
-        raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
-                    "equality_inference, path_finder: path = " ^
-                    space_implode " " (map string_of_int ps) ^
-                    " isa-term: " ^ Syntax.string_of_term ctxt tm ^
-                    (case t of
-                       SOME t => " fol-term: " ^ Metis_Term.toString t
-                     | NONE => ""))
+        raise METIS ("equality_inference (path_finder)",
+                     "path = " ^ space_implode " " (map string_of_int ps) ^
+                     " isa-term: " ^ Syntax.string_of_term ctxt tm ^
+                     (case t of
+                        SOME t => " fol-term: " ^ Metis_Term.toString t
+                      | NONE => ""))
       fun path_finder_FO tm [] = (tm, Bound 0)
         | path_finder_FO tm (p::ps) =
             let val (tm1,args) = strip_comb tm