src/Pure/IsaPlanner/isand.ML

       val ctypify = Thm.ctyp_of sgn
       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
       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;
     in Thm.instantiate (ctyfixes, []) th end;
 fun fix_vars_upto_idx ix th = 

       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
       val prop = (Thm.prop_of th);
       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;
     in Thm.instantiate ([], cfixes) th end;