Library.gen_merge_lists';
authorwenzelm
Sat, 24 Nov 2001 16:59:44 +0100
changeset 12290 29b1a4ef4d9f
parent 12289 ec2dafd0a6a9
child 12291 43f37745b600
Library.gen_merge_lists';
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