src/Pure/search.ML

 
 (*Searches until "satp" reports proof tree as satisfied.
   Suppresses duplicate solutions to minimize search space.*)
 fun DEPTH_FIRST satp tac = 
  let val tac = tracify trace_DEPTH_FIRST tac
-     fun depth used [] = None
+     fun depth used [] = NONE
        | depth used (q::qs) =
 	  case Seq.pull q of
-	      None         => depth used qs
-	    | Some(st,stq) => 
+	      NONE         => depth used qs
+	    | SOME(st,stq) => 
 		if satp st andalso not (gen_mem eq_thm (st, used))
-		then Some(st, Seq.make
+		then SOME(st, Seq.make
 			         (fn()=> depth (st::used) (stq::qs)))
 		else depth used (tac st :: stq :: qs)
   in  traced_tac (fn st => depth [] ([Seq.single st]))  end;
 
 

 		if !trace_DEPTH_FIRST then
 		    tracing (string_of_int np ^ 
 			     implode (map (fn _ => "*") qs))
 		else ();
 		Seq.pull q) of
-	     None         => depth (bnd,inc) qs
-	   | Some(st,stq) => 
+	     NONE         => depth (bnd,inc) qs
+	   | SOME(st,stq) => 
 	       if satp st	(*solution!*)
-	       then Some(st, Seq.make
+	       then SOME(st, Seq.make
 			 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
 
 	       else 
                let val np' = nprems_of st
 		     (*rgd' calculation assumes tactic operates on subgoal 1*)

 (*** Best-first search ***)
 
 val trace_BEST_FIRST = ref false;
 
 (*For creating output sequence*)
-fun some_of_list []     = None
-  | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
+fun some_of_list []     = NONE
+  | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
 
 (*Check for and delete duplicate proof states*)
 fun deleteAllMin prf heap = 
       if ThmHeap.is_empty heap then heap
       else if eq_thm (prf, #2 (ThmHeap.min heap))

 	   (case  partition satp news  of
 		([],nonsats) => next(foldr ThmHeap.insert
 					(map pairsize nonsats, nprf_heap)) 
 	      | (sats,_)  => some_of_list sats)
       and next nprf_heap =
-            if ThmHeap.is_empty nprf_heap then None
+            if ThmHeap.is_empty nprf_heap then NONE
 	    else 
 	    let val (n,prf) = ThmHeap.min nprf_heap
 	    in if !trace_BEST_FIRST 
 	       then tracing("state size = " ^ string_of_int n)  
                else ();

       else if  n=m andalso eq_thm(th,th')
               then (l',n,th')::nths
               else (l,m,th)::(l',n,th')::nths;
 
 (*For creating output sequence*)
-fun some_of_list []     = None
-  | some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l));
+fun some_of_list []     = NONE
+  | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
 
 val trace_ASTAR = ref false; 
 
 fun THEN_ASTAR tac0 (satp, costf) tac1 = 
   let val tf = tracify trace_ASTAR tac1;   

       in (case  partition satp news  of
             ([],nonsats) 
 		 => next (foldr insert_with_level (map cost nonsats, nprfs))
           | (sats,_)  => some_of_list sats)
       end and    
-      next []  = None
+      next []  = NONE
         | next ((level,n,prf)::nprfs)  =
             (if !trace_ASTAR 
                then tracing("level = " ^ string_of_int level ^
 			 "  cost = " ^ string_of_int n ^ 
                          "  queue length =" ^ string_of_int (length nprfs))