diff -r 94a794672c8b -r 26ead7ed4f4b src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Pure/tactic.ML	Mon Feb 26 23:18:24 2007 +0100
@@ -421,7 +421,7 @@
     foldr insert_tagged_brl netpair (taglist 1 brls);
 
 (*delete one kbrl from the pair of nets*)
-fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
+fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
 
 fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
   (if eres then