# HG changeset patch
# User wenzelm
# Date 1006617584 -3600
# Node ID 29b1a4ef4d9f58573efd7793ad4a8882d91f135f
# Parent  ec2dafd0a6a9592c71c9fb4e2e97a0c2bd36fd53
Library.gen_merge_lists';

diff -r ec2dafd0a6a9 -r 29b1a4ef4d9f src/Pure/Isar/net_rules.ML
--- 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