src/Pure/basis.ML
changeset 3244 71b760618f30
parent 3047 599cb28f8502
child 5021 235f8508d440
     1.1 --- a/src/Pure/basis.ML	Tue May 20 11:44:25 1997 +0200
     1.2 +++ b/src/Pure/basis.ML	Tue May 20 11:47:33 1997 +0200
     1.3 @@ -18,7 +18,8 @@
     1.4      | toString false = "false"
     1.5    end;
     1.6  
     1.7 -structure General =
     1.8 +
     1.9 +structure Option =
    1.10    struct
    1.11    exception Option
    1.12  
    1.13 @@ -34,8 +35,6 @@
    1.14      | valOf NONE     = raise Option
    1.15    end;
    1.16  
    1.17 -open General;
    1.18 -
    1.19  
    1.20  structure Int =
    1.21    struct
    1.22 @@ -75,11 +74,11 @@
    1.23  
    1.24    fun mapPartial f []      = []
    1.25      | mapPartial f (x::xs) = 
    1.26 -         (case f x of General.NONE   => mapPartial f xs
    1.27 -                    | General.SOME y => y :: mapPartial f xs);
    1.28 +         (case f x of Option.NONE   => mapPartial f xs
    1.29 +                    | Option.SOME y => y :: mapPartial f xs);
    1.30  
    1.31 -  fun find _ []        = General.NONE
    1.32 -    | find p (x :: xs) = if p x then General.SOME x else find p xs;
    1.33 +  fun find _ []        = Option.NONE
    1.34 +    | find p (x :: xs) = if p x then Option.SOME x else find p xs;
    1.35  
    1.36  
    1.37    (*copy the list preserving elements that satisfy the predicate*)