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