--- a/src/Pure/Isar/context_rules.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML Fri Feb 03 23:12:28 2006 +0100
@@ -104,9 +104,9 @@
Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
let
val wrappers =
- (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
- val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
- k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
+ (Library.merge (eq_snd (op =)) (ws1, ws2), Library.merge (eq_snd (op =)) (ws1', ws2'));
+ val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
+ k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
val next = ~ (length rules);
val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)