# HG changeset patch
# User wenzelm
# Date 938257538 -7200
# Node ID c97c3ad15d2eb2ecd8a7b25270057baec4a7581b
# Parent  5f5d575ddac331a4c373cfcc719b4e2b62d42b63
added fold_rule;

diff -r 5f5d575ddac3 -r c97c3ad15d2e src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Sep 24 17:18:51 1999 +0200
+++ b/src/Pure/tactic.ML	Sat Sep 25 13:05:38 1999 +0200
@@ -49,6 +49,7 @@
   val filt_resolve_tac	: thm list -> int -> int -> tactic
   val flexflex_tac	: tactic
   val fold_goals_tac	: thm list -> tactic
+  val fold_rule		: thm list -> thm -> thm
   val fold_tac		: thm list -> tactic
   val forward_tac	: thm list -> int -> tactic   
   val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
@@ -509,11 +510,11 @@
       val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
   in  map (keyfilter keylist) keys  end;
 
-fun fold_tac defs = EVERY 
-    (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
+val rev_defs = sort_lhs_depths o map symmetric;
 
-fun fold_goals_tac defs = EVERY 
-    (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
+fun fold_rule defs thm = 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