"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now

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