# HG changeset patch # User blanchet # Date 1302773045 -7200 # Node ID 4a58173ffb99568f54ad37e28173e474cc604c3d # Parent 118cc349de357d0650da7ce415533ec1e080a3a0 "unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now diff -r 118cc349de35 -r 4a58173ffb99 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 @@ -652,8 +652,9 @@ | (Var _, _) => add_terms (t, u) | (_, Var _) => add_terms (u, t) | _ => I - val t_inst = [] |> unify_terms (prem, concl) - |> map (pairself (cterm_of thy)) + val t_inst = + [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy))) + |> the_default [] (* FIXME *) in th |> cterm_instantiate t_inst end val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}