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/Pure/Proof/extraction.ML
changeset 18928 042608ffa2ec
parent 18921 f47c46d7d654
child 18956 c050ae1f8f52 
--- a/src/Pure/Proof/extraction.ML	Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Feb 06 11:01:28 2006 +0100
@@ -365,7 +365,7 @@
 
     val is_def =
       (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
-         (Const _, ts) => forall is_Var ts andalso null (duplicates ts)
+         (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
            andalso can (Thm.get_axiom_i thy) name
        | _ => false) handle TERM _ => false;
   in
isabelle