src/HOL/Hyperreal/transfer.ML
changeset 17432 835647238122
parent 17429 e8d6ed3aacfe
child 17956 369e2af8ee45
     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)