# HG changeset patch
# User blanchet
# Date 1284051023 -7200
# Node ID 6185c65c8a2b4cf8c73fc6be43481fa149724ef9
# Parent  c09c150f6af75385fb3a2c7d86af875aadf2a938
improve on 65903ec4e8e8: fix more "add_ffpair" exceptions in failed ATP proofs

diff -r c09c150f6af7 -r 6185c65c8a2b src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 09 18:22:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 09 18:50:23 2010 +0200
@@ -437,33 +437,30 @@
   could then fail. See comment on mk_var.*)
 fun resolve_inc_tyvars thy tha i thb =
   let
+    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
     fun aux tha thb =
-      let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha in
-        case Thm.bicompose false (false, tha, nprems_of tha) i thb
-             |> Seq.list_of |> distinct Thm.eq_thm of
-          [th] => th
-        | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
-                          [tha, thb])
-      end
+      case Thm.bicompose false (false, tha, nprems_of tha) i thb
+           |> Seq.list_of |> distinct Thm.eq_thm of
+        [th] => th
+      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
+                        [tha, thb])
   in
     aux tha thb
-    handle TERM _ =>
+    handle TERM z =>
            (* We could do it right the first time but this error occurs seldom
               and we don't want to break existing proofs in subtle ways or slow
               them down needlessly. *)
-           let
-             val ctyp_pairs =
-               [] |> fold (Term.add_vars o prop_of) [tha, thb]
-                  |> AList.group (op =)
-                  |> maps (fn ((s, _), T :: Ts) =>
-                              map (fn T' => (Free (s, T), Free (s, T'))) Ts)
-                  |> rpair (Envir.empty ~1)
-                  |-> fold (Pattern.unify thy)
-                  |> Envir.type_env |> Vartab.dest
-                  |> map (fn (x, (S, T)) =>
-                             pairself (ctyp_of thy) (TVar (x, S), T))
-             val repair = instantiate (ctyp_pairs, [])
-           in aux (repair tha) (repair thb) end
+           case [] |> fold (Term.add_vars o prop_of) [tha, thb]
+                   |> AList.group (op =)
+                   |> maps (fn ((s, _), T :: Ts) =>
+                               map (fn T' => (Free (s, T), Free (s, T'))) Ts)
+                   |> rpair (Envir.empty ~1)
+                   |-> fold (Pattern.unify thy)
+                   |> Envir.type_env |> Vartab.dest
+                   |> map (fn (x, (S, T)) =>
+                              pairself (ctyp_of thy) (TVar (x, S), T)) of
+             [] => raise TERM z
+           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
   end
 
 fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =