changeset 42354 | 79309a48a4a7 |
parent 42349 | 721e85fd2db3 |
child 42361 | 23f352990944 |
--- 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;