Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/classical.ML
changeset 22360 26ead7ed4f4b
parent 22095 07875394618e
child 22468 01751f5b0657 
--- a/src/Provers/classical.ML	Mon Feb 26 21:34:16 2007 +0100
+++ b/src/Provers/classical.ML	Mon Feb 26 23:18:24 2007 +0100
@@ -195,7 +195,7 @@
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes;
-    in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
+    in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
   else rule;
 
 
@@ -342,8 +342,8 @@
 fun delete x = delete_tagged_list (joinrules x);
 fun delete' x = delete_tagged_list (joinrules' x);
 
-val mem_thm = member Drule.eq_thm_prop
-and rem_thm = remove Drule.eq_thm_prop;
+val mem_thm = member Thm.eq_thm_prop
+and rem_thm = remove Thm.eq_thm_prop;
 
 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   is still allowed.*)
isabelle