tuned;
authorwenzelm
Tue Sep 13 22:19:35 2005 +0200 (2005-09-13 ago)
changeset 17351f7f2f56fcc28
parent 17350 26cd3756377a
child 17352 5bc9f8c81d58
tuned;
src/Pure/Isar/context_rules.ML
src/Pure/Isar/net_rules.ML
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue Sep 13 22:19:34 2005 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Sep 13 22:19:35 2005 +0200
     1.3 @@ -206,7 +206,7 @@
     1.4  
     1.5  fun gen_wrap which ctxt =
     1.6    let val Rules {wrappers, ...} = LocalRules.get ctxt
     1.7 -  in fn tac => foldr (fn ((w, _), t) => w t) tac (which wrappers) end;
     1.8 +  in fold_rev fst (which wrappers) end;
     1.9  
    1.10  val Swrap = gen_wrap #1;
    1.11  val wrap = gen_wrap #2;
     2.1 --- a/src/Pure/Isar/net_rules.ML	Tue Sep 13 22:19:34 2005 +0200
     2.2 +++ b/src/Pure/Isar/net_rules.ML	Tue Sep 13 22:19:35 2005 +0200
     2.3 @@ -51,7 +51,7 @@
     2.4  
     2.5  fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
     2.6    let val rules = Library.gen_merge_lists' eq rules1 rules2
     2.7 -  in foldr (uncurry add) (init eq index) rules end;
     2.8 +  in fold_rev add rules (init eq index) end;
     2.9  
    2.10  fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    2.11    if not (Library.gen_mem eq (rule, rules)) then rs