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/coherent.ML
changeset 29273 285c00993bc2
parent 28339 6f6fa16543f5 
--- a/src/Provers/coherent.ML	Wed Dec 31 18:53:17 2008 +0100
+++ b/src/Provers/coherent.ML	Wed Dec 31 18:53:18 2008 +0100
@@ -1,7 +1,6 @@
 (*  Title:      Provers/coherent.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
-                Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
+    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
 
 Prover for coherent logic, see e.g.
 
@@ -39,7 +38,7 @@
   ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
   int list * (term list * cl_prf) list;
 
-fun is_atomic t = null (term_consts t inter Data.operator_names);
+val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
 
 local open Conv in
isabelle