resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;
1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed May 29 18:52:35 2013 +0200
1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed May 29 18:55:37 2013 +0200
1.3 @@ -185,7 +185,7 @@
1.4 let
1.5 val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
1.6 fun aux (tha, thb) =
1.7 - case Thm.bicompose {flatten = true, match = false, incremented = false}
1.8 + case Thm.bicompose {flatten = true, match = false, incremented = true}
1.9 (false, tha, nprems_of tha) i thb
1.10 |> Seq.list_of |> distinct Thm.eq_thm of
1.11 [th] => th
1.12 @@ -193,7 +193,7 @@
1.13 [tha, thb])
1.14 in
1.15 aux (tha, thb)
1.16 - handle TERM z => (* FIXME obsolete!? *)
1.17 + handle TERM z =>
1.18 (* The unifier, which is invoked from "Thm.bicompose", will sometimes
1.19 refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
1.20 "TERM" exception (with "add_ffpair" as first argument). We then