src/Pure/Proof/extraction.ML
changeset 59787 6e2a20486897
parent 59582 0fbed69ff081
child 60826 695cf1fab6cc
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Mar 23 17:07:43 2015 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Mar 23 19:43:03 2015 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4          get_first (fn (_, (prems, (tm1, tm2))) =>
     1.5          let
     1.6            fun ren t = the_default t (Term.rename_abs tm1 tm t);
     1.7 -          val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
     1.8 +          val inc = Logic.incr_indexes ([], [], maxidx_of_term tm + 1);
     1.9            val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
    1.10            val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems;
    1.11            val env' = Envir.Envir