diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/Isar/context_rules.ML
--- 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))))