# HG changeset patch
# User blanchet
# Date 1307721129 -7200
# Node ID 2db277c6d506ab4cc6ee58019825bc8c53ba44bb
# Parent  ff6cfa33c65393b93db01add567066e815fb654e
tuning

diff -r ff6cfa33c653 -r 2db277c6d506 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jun 10 17:37:50 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jun 10 17:52:09 2011 +0200
@@ -180,14 +180,14 @@
 fun resolve_inc_tyvars thy tha i thb =
   let
     val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
-    fun aux tha thb =
+    fun aux (tha, thb) =
       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])
   in
-    aux tha thb
+    aux (tha, thb)
     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
@@ -206,7 +206,8 @@
                    |> map (fn (x, (S, T)) =>
                               pairself (ctyp_of thy) (TVar (x, S), T)) of
              [] => raise TERM z
-           | ps => aux (Drule.instantiate_normalize (ps, []) tha) (Drule.instantiate_normalize (ps, []) thb)
+           | ps => (tha, thb) |> pairself (Drule.instantiate_normalize (ps, []))
+                              |> aux
   end
 
 fun s_not (@{const Not} $ t) = t