src/Provers/classical.ML
changeset 19877 705ba8232952
parent 19257 4463aee061bc
child 20956 00fe22000c6a
     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