use mem operator
authorhuffman
Fri Sep 16 01:42:57 2005 +0200 (2005-09-16 ago)
changeset 17432835647238122
parent 17431 70311ad8bf11
child 17433 4cf2e7980529
use mem operator
src/HOL/Hyperreal/transfer.ML
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Fri Sep 16 01:34:53 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Fri Sep 16 01:42:57 2005 +0200
     1.3 @@ -47,8 +47,7 @@
     1.4  
     1.5  fun unstar_term consts term =
     1.6    let
     1.7 -    fun delete a = exists (fn x => x = a) consts
     1.8 -    fun unstar (Const(a,T) $ t) = if (delete a) then (unstar t)
     1.9 +    fun unstar (Const(a,T) $ t) = if (a mem consts) then (unstar t)
    1.10            else (Const(a,unstar_typ T) $ unstar t)
    1.11        | unstar (f $ t) = unstar f $ unstar t
    1.12        | unstar (Const(a,T)) = Const(a,unstar_typ T)