# HG changeset patch # User wenzelm # Date 1230745998 -3600 # Node ID 285c00993bc2e0631a6bcc6915da74732938c6c3 # Parent fb3ccf499df5f4ca09e8b1ac00c983bcaf3d238b use exists_Const directly; diff -r fb3ccf499df5 -r 285c00993bc2 src/HOL/ex/reflection.ML --- 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' diff -r fb3ccf499df5 -r 285c00993bc2 src/Provers/coherent.ML --- 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