# HG changeset patch
# User blanchet
# Date 1302773045 -7200
# Node ID 79309a48a4a7817245fc28d397ade6d154badb79
# Parent  7797efa897a1103ff36727b5239fdd65d691d3cd
nicer error message from Metis for know failure that isn't the user's fault

diff -r 7797efa897a1 -r 79309a48a4a7 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
@@ -424,6 +424,8 @@
         val _ = trace_msg ctxt (fn () => "  index_th2: " ^ string_of_int index_th2)
     in
       resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
+      handle TERM (s, _) => error ("Cannot replay Metis proof in Isabelle:\n" ^
+                                   "resolve_inf: " ^ s)
     end
   end;