--- a/src/Pure/Isar/context_rules.ML Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/Isar/context_rules.ML Mon Feb 26 23:18:24 2007 +0100
@@ -85,7 +85,7 @@
fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
let
- fun eq_th (_, (_, th')) = Drule.eq_thm_prop (th, th');
+ fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
in
if not (exists eq_th rules) then rs
@@ -106,7 +106,7 @@
val wrappers =
(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);
+ k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
val next = ~ (length rules);
val netpairs = fold (fn (n, (w, ((i, b), th))) =>
nth_map i (curry insert_tagged_brl ((w, n), (b, th))))