Basis library version of type "option" now resides in its own structure Option
authorpaulson
Tue May 20 11:47:33 1997 +0200 (1997-05-20)
changeset 324471b760618f30
parent 3243 a42653373043
child 3245 241838c01caf
Basis library version of type "option" now resides in its own structure Option
src/Provers/blast.ML
src/Pure/basis.ML
     1.1 --- a/src/Provers/blast.ML	Tue May 20 11:44:25 1997 +0200
     1.2 +++ b/src/Provers/blast.ML	Tue May 20 11:47:33 1997 +0200
     1.3 @@ -469,8 +469,6 @@
     1.4  
     1.5  fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
     1.6  
     1.7 -local open General in  (*make available the Basis type "option"*)
     1.8 -
     1.9  (*Tableau rule from elimination rule.  Flag "dup" requests duplication of the
    1.10    affected formula.*)
    1.11  fun fromRule vars rl = 
    1.12 @@ -480,13 +478,12 @@
    1.13  	  TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i
    1.14  	  THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
    1.15  	  
    1.16 -  in SOME (trl, tac) end
    1.17 +  in Option.SOME (trl, tac) end
    1.18    handle Bind => (*reject: conclusion is not just a variable*)
    1.19     (if !trace then (writeln"Warning: ignoring ill-formed elimination rule";
    1.20  		    print_thm rl)
    1.21      else ();
    1.22 -    NONE);
    1.23 -end;
    1.24 +    Option.NONE);
    1.25  
    1.26  
    1.27  (*** Conversion of Introduction Rules ***)
     2.1 --- a/src/Pure/basis.ML	Tue May 20 11:44:25 1997 +0200
     2.2 +++ b/src/Pure/basis.ML	Tue May 20 11:47:33 1997 +0200
     2.3 @@ -18,7 +18,8 @@
     2.4      | toString false = "false"
     2.5    end;
     2.6  
     2.7 -structure General =
     2.8 +
     2.9 +structure Option =
    2.10    struct
    2.11    exception Option
    2.12  
    2.13 @@ -34,8 +35,6 @@
    2.14      | valOf NONE     = raise Option
    2.15    end;
    2.16  
    2.17 -open General;
    2.18 -
    2.19  
    2.20  structure Int =
    2.21    struct
    2.22 @@ -75,11 +74,11 @@
    2.23  
    2.24    fun mapPartial f []      = []
    2.25      | mapPartial f (x::xs) = 
    2.26 -         (case f x of General.NONE   => mapPartial f xs
    2.27 -                    | General.SOME y => y :: mapPartial f xs);
    2.28 +         (case f x of Option.NONE   => mapPartial f xs
    2.29 +                    | Option.SOME y => y :: mapPartial f xs);
    2.30  
    2.31 -  fun find _ []        = General.NONE
    2.32 -    | find p (x :: xs) = if p x then General.SOME x else find p xs;
    2.33 +  fun find _ []        = Option.NONE
    2.34 +    | find p (x :: xs) = if p x then Option.SOME x else find p xs;
    2.35  
    2.36  
    2.37    (*copy the list preserving elements that satisfy the predicate*)