# HG changeset patch
# User wenzelm
# Date 1369846537 -7200
# Node ID 568b2cd65d50f143c2245629837955aacda7a7db
# Parent  6ba76ad4e679a98195b3482590072324ac600c51
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;

diff -r 6ba76ad4e679 -r 568b2cd65d50 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 29 18:52:35 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 29 18:55:37 2013 +0200
@@ -185,7 +185,7 @@
   let
     val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
     fun aux (tha, thb) =
-      case Thm.bicompose {flatten = true, match = false, incremented = false}
+      case Thm.bicompose {flatten = true, match = false, incremented = true}
             (false, tha, nprems_of tha) i thb
            |> Seq.list_of |> distinct Thm.eq_thm of
         [th] => th
@@ -193,7 +193,7 @@
                         [tha, thb])
   in
     aux (tha, thb)
-    handle TERM z =>  (* FIXME obsolete!? *)
+    handle TERM z =>
            (* The unifier, which is invoked from "Thm.bicompose", will sometimes
               refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
               "TERM" exception (with "add_ffpair" as first argument). We then