src/Pure/Proof/extraction.ML
changeset 32032 a6a6e8031c14
parent 30718 15041c7e51e4
child 32035 8e77b6a250d5
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Jul 17 21:33:00 2009 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Jul 17 21:33:00 2009 +0200
     1.3 @@ -105,9 +105,8 @@
     1.4            val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
     1.5            val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
     1.6            val env' = Envir.Envir
     1.7 -            {maxidx = Library.foldl Int.max
     1.8 -              (~1, map (Int.max o pairself maxidx_of_term) prems'),
     1.9 -             iTs = Tenv, asol = tenv};
    1.10 +            {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
    1.11 +             tenv = tenv, tyenv = Tenv};
    1.12            val env'' = fold (Pattern.unify thy o pairself (lookup rew)) prems' env';
    1.13          in SOME (Envir.norm_term env'' (inc (ren tm2)))
    1.14          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)