1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -424,6 +424,8 @@
     1.4          val _ = trace_msg ctxt (fn () => "  index_th2: " ^ string_of_int index_th2)
     1.5      in
     1.6        resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
     1.7 +      handle TERM (s, _) => error ("Cannot replay Metis proof in Isabelle:\n" ^
     1.8 +                                   "resolve_inf: " ^ s)
     1.9      end
    1.10    end;
    1.11