diff -r 70311ad8bf11 -r 835647238122 src/HOL/Hyperreal/transfer.ML
--- a/src/HOL/Hyperreal/transfer.ML	Fri Sep 16 01:34:53 2005 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Fri Sep 16 01:42:57 2005 +0200
@@ -47,8 +47,7 @@
 
 fun unstar_term consts term =
   let
-    fun delete a = exists (fn x => x = a) consts
-    fun unstar (Const(a,T) $ t) = if (delete a) then (unstar t)
+    fun unstar (Const(a,T) $ t) = if (a mem consts) then (unstar t)
           else (Const(a,unstar_typ T) $ unstar t)
       | unstar (f $ t) = unstar f $ unstar t
       | unstar (Const(a,T)) = Const(a,unstar_typ T)