src/Pure/basis.ML
changeset 3244 71b760618f30
parent 3047 599cb28f8502
child 5021 235f8508d440
--- a/src/Pure/basis.ML	Tue May 20 11:44:25 1997 +0200
+++ b/src/Pure/basis.ML	Tue May 20 11:47:33 1997 +0200
@@ -18,7 +18,8 @@
     | toString false = "false"
   end;
 
-structure General =
+
+structure Option =
   struct
   exception Option
 
@@ -34,8 +35,6 @@
     | valOf NONE     = raise Option
   end;
 
-open General;
-
 
 structure Int =
   struct
@@ -75,11 +74,11 @@
 
   fun mapPartial f []      = []
     | mapPartial f (x::xs) = 
-         (case f x of General.NONE   => mapPartial f xs
-                    | General.SOME y => y :: mapPartial f xs);
+         (case f x of Option.NONE   => mapPartial f xs
+                    | Option.SOME y => y :: mapPartial f xs);
 
-  fun find _ []        = General.NONE
-    | find p (x :: xs) = if p x then General.SOME x else find p xs;
+  fun find _ []        = Option.NONE
+    | find p (x :: xs) = if p x then Option.SOME x else find p xs;
 
 
   (*copy the list preserving elements that satisfy the predicate*)