# HG changeset patch
# User wenzelm
# Date 1437858937 -7200
# Node ID 7e2c8a63a8f8bb6396db191aa2e34b8ee7dc30f8
# Parent  c4d3da84d8841fbc2e01e0cb9b1dbbbb0254e398
more accurate maxidx;

diff -r c4d3da84d884 -r 7e2c8a63a8f8 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Jul 25 21:54:09 2015 +0200
+++ b/src/Pure/drule.ML	Sat Jul 25 23:15:37 2015 +0200
@@ -761,9 +761,11 @@
           let
             val T = var_type xi;
             val U = Thm.typ_of_cterm cu;
-            val (tyenv', maxidx') =
-              Sign.typ_unify thy (T, U)
-                (tyenv, maxidx |> Integer.max (#2 xi) |> Integer.max (Thm.maxidx_of_cterm cu))
+            val maxidx' = maxidx
+              |> Integer.max (#2 xi)
+              |> Term.maxidx_typ T
+              |> Integer.max (Thm.maxidx_of_cterm cu);
+            val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx')
               handle Type.TUNIFY =>
                 let
                   val t = Var (xi, T);
@@ -777,7 +779,7 @@
                     Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u),
                     0, [th])
                 end;
-          in (((xi, T), cu), (tyenv', maxidx')) end;
+          in (((xi, T), cu), (tyenv', maxidx'')) end;
 
         val (args', (tyenv, _)) = fold_map infer args (Vartab.empty, 0);
         val instT =