src/Pure/type_infer.ML
changeset 19482 9f11af8f7ef9
parent 19465 e6093a7fa53a
child 19577 fdb3642feb49
     1.1 --- a/src/Pure/type_infer.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -413,7 +413,7 @@
     1.4      (*collect result unifier*)
     1.5      fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE)
     1.6        | ch_var xi_T = SOME xi_T;
     1.7 -    val env = List.mapPartial ch_var Tps;
     1.8 +    val env = map_filter ch_var Tps;
     1.9  
    1.10      (*convert back to terms/typs*)
    1.11      val mk_var =