# HG changeset patch
# User paulson
# Date 864121653 -7200
# Node ID 71b760618f30daba567fa96bf634cab83add3420
# Parent  a42653373043ec1c26f145ea3ddcf423ea98d78a
Basis library version of type "option" now resides in its own structure Option

diff -r a42653373043 -r 71b760618f30 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue May 20 11:44:25 1997 +0200
+++ b/src/Provers/blast.ML	Tue May 20 11:47:33 1997 +0200
@@ -469,8 +469,6 @@
 
 fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
 
-local open General in  (*make available the Basis type "option"*)
-
 (*Tableau rule from elimination rule.  Flag "dup" requests duplication of the
   affected formula.*)
 fun fromRule vars rl = 
@@ -480,13 +478,12 @@
 	  TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i
 	  THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
 	  
-  in SOME (trl, tac) end
+  in Option.SOME (trl, tac) end
   handle Bind => (*reject: conclusion is not just a variable*)
    (if !trace then (writeln"Warning: ignoring ill-formed elimination rule";
 		    print_thm rl)
     else ();
-    NONE);
-end;
+    Option.NONE);
 
 
 (*** Conversion of Introduction Rules ***)
diff -r a42653373043 -r 71b760618f30 src/Pure/basis.ML
--- 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*)