# HG changeset patch
# User blanchet
# Date 1283966557 -7200
# Node ID 65903ec4e8e868cd146f9ca3b4149854863b1a65
# Parent  eec61233dbad9d18fb0a681ed6b67cee887c855b
workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer;
to reproduce the old bug, replace the command
 by(rule new_Addr_SomeD)
on line 27 of Jinja/J/TypeSafe.thy with
 by (metis new_Addr_SomeD)

diff -r eec61233dbad -r 65903ec4e8e8 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Sep 08 19:20:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Sep 08 19:22:37 2010 +0200
@@ -435,18 +435,40 @@
 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
   of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
   could then fail. See comment on mk_var.*)
-fun resolve_inc_tyvars(tha,i,thb) =
+fun resolve_inc_tyvars thy tha i thb =
   let
-      val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
-      val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
+    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
   in
-      case distinct Thm.eq_thm ths of
-        [th] => th
-      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
+    aux tha thb
+    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
   end
 
 fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
   let
+    val thy = ProofContext.theory_of ctxt
     val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
     val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
     val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
@@ -466,7 +488,10 @@
         val index_th2 = get_index i_atm prems_th2
               handle Empty => raise Fail "Failed to find literal in th2"
         val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
-    in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
+    in
+      resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
+                         i_th2
+    end
   end;
 
 (* INFERENCE RULE: REFL *)