# HG changeset patch
# User blanchet
# Date 1284051235 -7200
# Node ID c663b0cdebc411815b9411bf70df954c0dc31d14
# Parent  6185c65c8a2b4cf8c73fc6be43481fa149724ef9
clarify comment

diff -r 6185c65c8a2b -r c663b0cdebc4 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 09 18:50:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 09 18:53:55 2010 +0200
@@ -432,9 +432,9 @@
 
 (* INFERENCE RULE: RESOLVE *)
 
-(*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.*)
+(* 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 thy tha i thb =
   let
     val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
@@ -447,9 +447,13 @@
   in
     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. *)
+           (* 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
+              perform unification of the types of variables by hand and try
+              again. We could do this the first time around but this error
+              occurs seldom and we don't want to break existing proofs in subtle
+              ways or slow them down needlessly. *)
            case [] |> fold (Term.add_vars o prop_of) [tha, thb]
                    |> AList.group (op =)
                    |> maps (fn ((s, _), T :: Ts) =>