use exists_Const directly;

--- a/src/HOL/ex/reflection.ML	Wed Dec 31 18:53:17 2008 +0100
+++ b/src/HOL/ex/reflection.ML	Wed Dec 31 18:53:18 2008 +0100
@@ -40,7 +40,7 @@
        if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
        else add_fterms t1 #> add_fterms t2
      | add_fterms (t as Abs(xn,xT,t')) = 
-       if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
+       if exists_Const (fn (c, _) => c = fN) t then (fn _ => [t]) else (fn _ => [])
      | add_fterms _ = I
    val fterms = add_fterms rhs []
    val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt'

--- 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