more accurate maxidx;
authorwenzelm
Sat Jul 25 23:15:37 2015 +0200 (2015-07-25)
changeset 607807e2c8a63a8f8
parent 60779 c4d3da84d884
child 60781 2da59cdf531c
more accurate maxidx;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Sat Jul 25 21:54:09 2015 +0200
     1.2 +++ b/src/Pure/drule.ML	Sat Jul 25 23:15:37 2015 +0200
     1.3 @@ -761,9 +761,11 @@
     1.4            let
     1.5              val T = var_type xi;
     1.6              val U = Thm.typ_of_cterm cu;
     1.7 -            val (tyenv', maxidx') =
     1.8 -              Sign.typ_unify thy (T, U)
     1.9 -                (tyenv, maxidx |> Integer.max (#2 xi) |> Integer.max (Thm.maxidx_of_cterm cu))
    1.10 +            val maxidx' = maxidx
    1.11 +              |> Integer.max (#2 xi)
    1.12 +              |> Term.maxidx_typ T
    1.13 +              |> Integer.max (Thm.maxidx_of_cterm cu);
    1.14 +            val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx')
    1.15                handle Type.TUNIFY =>
    1.16                  let
    1.17                    val t = Var (xi, T);
    1.18 @@ -777,7 +779,7 @@
    1.19                      Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u),
    1.20                      0, [th])
    1.21                  end;
    1.22 -          in (((xi, T), cu), (tyenv', maxidx')) end;
    1.23 +          in (((xi, T), cu), (tyenv', maxidx'')) end;
    1.24  
    1.25          val (args', (tyenv, _)) = fold_map infer args (Vartab.empty, 0);
    1.26          val instT =