src/Pure/Proof/extraction.ML
changeset 32035 8e77b6a250d5
parent 32032 a6a6e8031c14
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Jul 17 22:54:11 2009 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Jul 17 23:11:40 2009 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4            fun ren t = the_default t (Term.rename_abs tm1 tm t);
     1.5            val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
     1.6            val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
     1.7 -          val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
     1.8 +          val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems;
     1.9            val env' = Envir.Envir
    1.10              {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
    1.11               tenv = tenv, tyenv = Tenv};