diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/IsaPlanner/isand.ML
--- a/src/Pure/IsaPlanner/isand.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/IsaPlanner/isand.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -257,7 +257,7 @@
       val prop = (Thm.prop_of th);
       val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
       val ctyfixes = 
-          Library.mapfilter 
+          map_filter 
             (fn (v as ((s,i),ty)) => 
                 if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
                 else NONE) tvars;
@@ -271,7 +271,7 @@
       val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
                                                [] (prop :: tpairs));
       val cfixes = 
-          Library.mapfilter 
+          map_filter 
             (fn (v as ((s,i),ty)) => 
                 if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
                 else NONE) vars;