src/Pure/Isar/net_rules.ML
changeset 17351 f7f2f56fcc28
parent 16800 90eff1b52428
child 18646 612dcdd9c03d
     1.1 --- a/src/Pure/Isar/net_rules.ML	Tue Sep 13 22:19:34 2005 +0200
     1.2 +++ b/src/Pure/Isar/net_rules.ML	Tue Sep 13 22:19:35 2005 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5  fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
     1.6    let val rules = Library.gen_merge_lists' eq rules1 rules2
     1.7 -  in foldr (uncurry add) (init eq index) rules end;
     1.8 +  in fold_rev add rules (init eq index) end;
     1.9  
    1.10  fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    1.11    if not (Library.gen_mem eq (rule, rules)) then rs