# 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 =