diff -r a6205c6203ea -r 9f11af8f7ef9 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Provers/blast.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -538,16 +538,12 @@
   case P of
       (Const ("*Goal*", _) $ G) =>
         let val pG = mk_Trueprop (toTerm 2 G)
-            val intrs = List.concat
-                             (map (fn (inet,_) => Net.unify_term inet pG)
-                              nps)
+            val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
         in  map (fromIntrRule vars o #2) (Tactic.orderlist intrs)  end
     | _ =>
         let val pP = mk_Trueprop (toTerm 3 P)
-            val elims = List.concat
-                             (map (fn (_,enet) => Net.unify_term enet pP)
-                              nps)
-        in  List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims)  end;
+            val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
+        in  map_filter (fromRule vars o #2) (Tactic.orderlist elims)  end;
 
 
 (*Pending formulae carry md (may duplicate) flags*)