Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hyperreal/transfer.ML
changeset 17432 835647238122
parent 17429 e8d6ed3aacfe
child 17956 369e2af8ee45 
--- 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)
isabelle