src/Pure/tactic.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15671 8df681866dc9
     1.1 --- a/src/Pure/tactic.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/Pure/tactic.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -426,7 +426,7 @@
     1.4  
     1.5  (*build a pair of nets for biresolution*)
     1.6  fun build_netpair netpair brls =
     1.7 -    Library.foldr insert_tagged_brl (taglist 1 brls, netpair);
     1.8 +    foldr insert_tagged_brl netpair (taglist 1 brls);
     1.9  
    1.10  (*delete one kbrl from the pair of nets*)
    1.11  local
    1.12 @@ -473,7 +473,7 @@
    1.13  
    1.14  (*build a net of rules for resolution*)
    1.15  fun build_net rls =
    1.16 -    Library.foldr insert_krl (taglist 1 rls, Net.empty);
    1.17 +    foldr insert_krl Net.empty (taglist 1 rls);
    1.18  
    1.19  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
    1.20  fun filt_resolution_from_net_tac match pred net =
    1.21 @@ -644,7 +644,7 @@
    1.22      val statement = Logic.list_implies (asms, prop);
    1.23      val frees = map Term.dest_Free (Term.term_frees statement);
    1.24      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
    1.25 -    val fixed_tfrees = Library.foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
    1.26 +    val fixed_tfrees = foldr Term.add_typ_tfree_names [] (map #2 fixed_frees);
    1.27      val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
    1.28  
    1.29      fun err msg = raise ERROR_MESSAGE