--- 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 *)