--- a/src/Pure/pattern.ML Fri Jul 17 22:54:11 2009 +0200
+++ b/src/Pure/pattern.ML Fri Jul 17 23:11:40 2009 +0200
@@ -354,7 +354,7 @@
Abs(ns,Ts,ts) =>
(case obj of
Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env
- | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
+ | _ => let val Tt = Envir.subst_type iTs Ts
in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end)
| _ => (case obj of
Abs(nt,Tt,tt) =>
@@ -428,7 +428,7 @@
fun match_rew thy tm (tm1, tm2) =
let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
- SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
+ SOME (Envir.subst_term (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
handle MATCH => NONE
end;