src/Pure/pattern.ML
changeset 19482 9f11af8f7ef9
parent 19300 7689f81f8996
child 19502 369cde91963d
     1.1 --- a/src/Pure/pattern.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/pattern.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -177,7 +177,7 @@
     1.4                        let val js = ints_of' env ts;
     1.5                            val js' = map (try (trans d)) js;
     1.6                            val ks = mk_proj_list js';
     1.7 -                          val ls = List.mapPartial I js'
     1.8 +                          val ls = map_filter I js'
     1.9                            val Hty = type_of_G env (Fty,length js,ks)
    1.10                            val (env',H) = Envir.genvar a (env,Hty)
    1.11                            val env'' =