changeset 19877 | 705ba8232952 |
parent 19257 | 4463aee061bc |
child 20956 | 00fe22000c6a |
--- 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;