183 Instantiations of those Vars could then fail. *) |
183 Instantiations of those Vars could then fail. *) |
184 fun resolve_inc_tyvars thy tha i thb = |
184 fun resolve_inc_tyvars thy tha i thb = |
185 let |
185 let |
186 val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha |
186 val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha |
187 fun aux (tha, thb) = |
187 fun aux (tha, thb) = |
188 case Thm.bicompose false (false, tha, nprems_of tha) i thb |
188 case Thm.bicompose {flatten = true, match = false, incremented = false} |
|
189 (false, tha, nprems_of tha) i thb |
189 |> Seq.list_of |> distinct Thm.eq_thm of |
190 |> Seq.list_of |> distinct Thm.eq_thm of |
190 [th] => th |
191 [th] => th |
191 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, |
192 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, |
192 [tha, thb]) |
193 [tha, thb]) |
193 in |
194 in |
194 aux (tha, thb) |
195 aux (tha, thb) |
195 handle TERM z => |
196 handle TERM z => (* FIXME obsolete!? *) |
196 (* The unifier, which is invoked from "Thm.bicompose", will sometimes |
197 (* The unifier, which is invoked from "Thm.bicompose", will sometimes |
197 refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a |
198 refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a |
198 "TERM" exception (with "add_ffpair" as first argument). We then |
199 "TERM" exception (with "add_ffpair" as first argument). We then |
199 perform unification of the types of variables by hand and try |
200 perform unification of the types of variables by hand and try |
200 again. We could do this the first time around but this error |
201 again. We could do this the first time around but this error |