src/Pure/tactic.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/Pure/tactic.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -368,7 +368,7 @@
     1.4  
     1.5  (*As above, but inserts only facts (unconditional theorems);
     1.6    generates no additional subgoals. *)
     1.7 -fun cut_facts_tac ths = cut_rules_tac  (filter is_fact ths);
     1.8 +fun cut_facts_tac ths = cut_rules_tac  (List.filter is_fact ths);
     1.9  
    1.10  (*Introduce the given proposition as a lemma and subgoal*)
    1.11  fun subgoal_tac sprop =
    1.12 @@ -426,7 +426,7 @@
    1.13  
    1.14  (*build a pair of nets for biresolution*)
    1.15  fun build_netpair netpair brls =
    1.16 -    foldr insert_tagged_brl (taglist 1 brls, netpair);
    1.17 +    Library.foldr insert_tagged_brl (taglist 1 brls, netpair);
    1.18  
    1.19  (*delete one kbrl from the pair of nets*)
    1.20  local
    1.21 @@ -473,7 +473,7 @@
    1.22  
    1.23  (*build a net of rules for resolution*)
    1.24  fun build_net rls =
    1.25 -    foldr insert_krl (taglist 1 rls, Net.empty);
    1.26 +    Library.foldr insert_krl (taglist 1 rls, Net.empty);
    1.27  
    1.28  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
    1.29  fun filt_resolution_from_net_tac match pred net =
    1.30 @@ -562,7 +562,7 @@
    1.31  
    1.32  val rev_defs = sort_lhs_depths o map symmetric;
    1.33  
    1.34 -fun fold_rule defs thm = foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
    1.35 +fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
    1.36  fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
    1.37  fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
    1.38  
    1.39 @@ -620,7 +620,7 @@
    1.40          else (Then tac (rotate_tac n THEN' etac thin_rl),0);
    1.41    in SUBGOAL(fn (subg,n) =>
    1.42         let val Hs = Logic.strip_assums_hyp subg
    1.43 -       in case fst(foldl thins ((NONE,0),Hs)) of
    1.44 +       in case fst(Library.foldl thins ((NONE,0),Hs)) of
    1.45              NONE => no_tac | SOME tac => tac n
    1.46         end)
    1.47    end;
    1.48 @@ -644,8 +644,8 @@
    1.49      val statement = Logic.list_implies (asms, prop);
    1.50      val frees = map Term.dest_Free (Term.term_frees statement);
    1.51      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
    1.52 -    val fixed_tfrees = foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
    1.53 -    val params = mapfilter (fn x => apsome (pair x) (assoc_string (frees, x))) xs;
    1.54 +    val fixed_tfrees = Library.foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
    1.55 +    val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
    1.56  
    1.57      fun err msg = raise ERROR_MESSAGE
    1.58        (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^