changeset 12290 | 29b1a4ef4d9f |
parent 11776 | d4f9de0bde28 |
child 12385 | 389d11fb62c8 |
--- a/src/Pure/Isar/net_rules.ML Sat Nov 24 16:59:32 2001 +0100 +++ b/src/Pure/Isar/net_rules.ML Sat Nov 24 16:59:44 2001 +0100 @@ -64,7 +64,7 @@ fun merge (Rules {eq, weight, index, rules = rules1, ...}, Rules {rules = rules2, ...}) = - make eq weight index (Library.generic_merge eq I I rules1 rules2); + make eq weight index (Library.gen_merge_lists' eq rules1 rules2); fun delete rule (rs as Rules {eq, weight, index, rules, next, net}) = if not (Library.gen_mem eq (rule, rules)) then rs