# HG changeset patch
# User wenzelm
# Date 1126642775 -7200
# Node ID f7f2f56fcc28a3726c3fb2a6aa0aebe14df6ac52
# Parent  26cd3756377a8d742814fcea219e732dc7b4937b
tuned;

diff -r 26cd3756377a -r f7f2f56fcc28 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue Sep 13 22:19:34 2005 +0200
+++ b/src/Pure/Isar/context_rules.ML	Tue Sep 13 22:19:35 2005 +0200
@@ -206,7 +206,7 @@
 
 fun gen_wrap which ctxt =
   let val Rules {wrappers, ...} = LocalRules.get ctxt
-  in fn tac => foldr (fn ((w, _), t) => w t) tac (which wrappers) end;
+  in fold_rev fst (which wrappers) end;
 
 val Swrap = gen_wrap #1;
 val wrap = gen_wrap #2;
diff -r 26cd3756377a -r f7f2f56fcc28 src/Pure/Isar/net_rules.ML
--- a/src/Pure/Isar/net_rules.ML	Tue Sep 13 22:19:34 2005 +0200
+++ b/src/Pure/Isar/net_rules.ML	Tue Sep 13 22:19:35 2005 +0200
@@ -51,7 +51,7 @@
 
 fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
   let val rules = Library.gen_merge_lists' eq rules1 rules2
-  in foldr (uncurry add) (init eq index) rules end;
+  in fold_rev add rules (init eq index) end;
 
 fun delete rule (rs as Rules {eq, index, rules, next, net}) =
   if not (Library.gen_mem eq (rule, rules)) then rs