src/Pure/pattern.ML

--- a/src/Pure/pattern.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/pattern.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -177,7 +177,7 @@
                       let val js = ints_of' env ts;
                           val js' = map (try (trans d)) js;
                           val ks = mk_proj_list js';
-                          val ls = List.mapPartial I js'
+                          val ls = map_filter I js'
                           val Hty = type_of_G env (Fty,length js,ks)
                           val (env',H) = Envir.genvar a (env,Hty)
                           val env'' =