src/Provers/classical.ML
changeset 22360 26ead7ed4f4b
parent 22095 07875394618e
child 22468 01751f5b0657
     1.1 --- a/src/Provers/classical.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/Provers/classical.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -195,7 +195,7 @@
     1.4            else all_tac))
     1.5          |> Seq.hd
     1.6          |> Drule.zero_var_indexes;
     1.7 -    in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
     1.8 +    in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
     1.9    else rule;
    1.10  
    1.11  
    1.12 @@ -342,8 +342,8 @@
    1.13  fun delete x = delete_tagged_list (joinrules x);
    1.14  fun delete' x = delete_tagged_list (joinrules' x);
    1.15  
    1.16 -val mem_thm = member Drule.eq_thm_prop
    1.17 -and rem_thm = remove Drule.eq_thm_prop;
    1.18 +val mem_thm = member Thm.eq_thm_prop
    1.19 +and rem_thm = remove Thm.eq_thm_prop;
    1.20  
    1.21  (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
    1.22    is still allowed.*)