# 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}