src/Pure/tactic.ML
changeset 7596 c97c3ad15d2e
parent 7491 95a4af0e10a7
child 8129 29e239c7b8c2
     1.1 --- a/src/Pure/tactic.ML	Fri Sep 24 17:18:51 1999 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sat Sep 25 13:05:38 1999 +0200
     1.3 @@ -49,6 +49,7 @@
     1.4    val filt_resolve_tac	: thm list -> int -> int -> tactic
     1.5    val flexflex_tac	: tactic
     1.6    val fold_goals_tac	: thm list -> tactic
     1.7 +  val fold_rule		: thm list -> thm -> thm
     1.8    val fold_tac		: thm list -> tactic
     1.9    val forward_tac	: thm list -> int -> tactic   
    1.10    val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
    1.11 @@ -509,11 +510,11 @@
    1.12        val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
    1.13    in  map (keyfilter keylist) keys  end;
    1.14  
    1.15 -fun fold_tac defs = EVERY 
    1.16 -    (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
    1.17 +val rev_defs = sort_lhs_depths o map symmetric;
    1.18  
    1.19 -fun fold_goals_tac defs = EVERY 
    1.20 -    (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
    1.21 +fun fold_rule defs thm = foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
    1.22 +fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
    1.23 +fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
    1.24  
    1.25  
    1.26  (*** Renaming of parameters in a subgoal