Drule.equiv_thm supercedes Drule.weak_eq_thm;
authorwenzelm
Tue Jun 13 23:41:41 2006 +0200 (2006-06-13)
changeset 19877705ba8232952
parent 19876 11d447d5d68c
child 19878 51ae6677dd5f
Drule.equiv_thm supercedes Drule.weak_eq_thm;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Tue Jun 13 23:41:39 2006 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Jun 13 23:41:41 2006 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4          |> Seq.hd
     1.5          |> Drule.zero_var_indexes
     1.6          |> Thm.put_name_tags (Thm.get_name_tags rule);
     1.7 -    in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end
     1.8 +    in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
     1.9    else rule;
    1.10  
    1.11