# HG changeset patch
# User wenzelm
# Date 1150234901 -7200
# Node ID 705ba82329525276879851f79d8c510a6f256c48
# Parent  11d447d5d68cae9d8139af559f01ef34e6b915eb
Drule.equiv_thm supercedes Drule.weak_eq_thm;

diff -r 11d447d5d68c -r 705ba8232952 src/Provers/classical.ML
--- 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;