nicer error message from Metis for know failure that isn't the user's fault

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