src/Pure/tactic.ML

   subgoals.*)
 fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
 
 (*As above, but inserts only facts (unconditional theorems);
   generates no additional subgoals. *)
-fun cut_facts_tac ths = cut_rules_tac  (filter is_fact ths);
+fun cut_facts_tac ths = cut_rules_tac  (List.filter is_fact ths);
 
 (*Introduce the given proposition as a lemma and subgoal*)
 fun subgoal_tac sprop =
   DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
     let val concl' = Logic.strip_assums_concl prop in

     | NONE => error "insert_tagged_brl: elimination rule with no premises")
   else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
 
 (*build a pair of nets for biresolution*)
 fun build_netpair netpair brls =
-    foldr insert_tagged_brl (taglist 1 brls, netpair);
+    Library.foldr insert_tagged_brl (taglist 1 brls, netpair);
 
 (*delete one kbrl from the pair of nets*)
 local
   fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
 in

 fun insert_krl (krl as (k,th), net) =
     Net.insert_term ((concl_of th, krl), net, K false);
 
 (*build a net of rules for resolution*)
 fun build_net rls =
-    foldr insert_krl (taglist 1 rls, Net.empty);
+    Library.foldr insert_krl (taglist 1 rls, Net.empty);
 
 (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
 fun filt_resolution_from_net_tac match pred net =
   SUBGOAL
     (fn (prem,i) =>

       val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
   in  map (keyfilter keylist) keys  end;
 
 val rev_defs = sort_lhs_depths o map symmetric;
 
-fun fold_rule defs thm = foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
+fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
 fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
 
 
 (*** Renaming of parameters in a subgoal

       fun thins ((tac,n),H) =
         if p H then (tac,n+1)
         else (Then tac (rotate_tac n THEN' etac thin_rl),0);
   in SUBGOAL(fn (subg,n) =>
        let val Hs = Logic.strip_assums_hyp subg
-       in case fst(foldl thins ((NONE,0),Hs)) of
+       in case fst(Library.foldl thins ((NONE,0),Hs)) of
             NONE => no_tac | SOME tac => tac n
        end)
   end;
 
 

 fun prove sign xs asms prop tac =
   let
     val statement = Logic.list_implies (asms, prop);
     val frees = map Term.dest_Free (Term.term_frees statement);
     val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
-    val fixed_tfrees = foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
-    val params = mapfilter (fn x => apsome (pair x) (assoc_string (frees, x))) xs;
+    val fixed_tfrees = Library.foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
+    val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
 
     fun err msg = raise ERROR_MESSAGE
       (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
         Sign.string_of_term sign (Term.list_all_free (params, statement)));