| changeset 32035 | 8e77b6a250d5 |
| parent 29606 | fedb8be05f24 |
| child 32050 | ebb9274e34b7 |
--- a/src/Pure/defs.ML Fri Jul 17 22:54:11 2009 +0200 +++ b/src/Pure/defs.ML Fri Jul 17 23:11:40 2009 +0200 @@ -46,7 +46,7 @@ handle Type.TUNIFY => true); fun match_args (Ts, Us) = - Option.map Envir.typ_subst_TVars + Option.map Envir.subst_type (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);