Drule.equiv_thm supercedes Drule.weak_eq_thm;

--- a/src/Provers/classical.ML	Tue Jun 13 23:41:39 2006 +0200
+++ b/src/Provers/classical.ML	Tue Jun 13 23:41:41 2006 +0200
@@ -196,7 +196,7 @@
         |> Seq.hd
         |> Drule.zero_var_indexes
         |> Thm.put_name_tags (Thm.get_name_tags rule);
-    in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end
+    in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
   else rule;