src/Pure/tctical.ML

 (*The tactical ORELSE uses the first tactic that returns a nonempty sequence.
   Like in LCF, ORELSE commits to either tac1 or tac2 immediately.
   Does not backtrack to tac2 if tac1 was initially chosen. *)
 fun (tac1 ORELSE tac2) st =
     case Seq.pull(tac1 st) of
-        None       => tac2 st
+        NONE       => tac2 st
       | sequencecell => Seq.make(fn()=> sequencecell);
 
 
 (*The tactical APPEND combines the results of two tactics.
   Like ORELSE, but allows backtracking on both tac1 and tac2.

         tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
         tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
 *)
 fun (tac THEN_ELSE (tac1, tac2)) st =
     case Seq.pull(tac st) of
-        None    => tac2 st              (*failed; try tactic 2*)
+        NONE    => tac2 st              (*failed; try tactic 2*)
       | seqcell => Seq.flat       (*succeeded; use tactic 1*)
                     (Seq.map tac1 (Seq.make(fn()=> seqcell)));
 
 
 (*Versions for combining tactic-valued functions, as in

 
 local
   (*This version of EVERY avoids backtracking over repeated states*)
 
   fun EVY (trail, []) st =
-        Seq.make (fn()=> Some(st,
+        Seq.make (fn()=> SOME(st,
                         Seq.make (fn()=> Seq.pull (evyBack trail))))
     | EVY (trail, tac::tacs) st =
           case Seq.pull(tac st) of
-              None    => evyBack trail              (*failed: backtrack*)
-            | Some(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
+              NONE    => evyBack trail              (*failed: backtrack*)
+            | SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st'
   and evyBack [] = Seq.empty (*no alternatives*)
     | evyBack ((st',q,tacs)::trail) =
           case Seq.pull q of
-              None        => evyBack trail
-            | Some(st,q') => if eq_thm (st',st)
+              NONE        => evyBack trail
+            | SOME(st,q') => if eq_thm (st',st)
                              then evyBack ((st',q',tacs)::trail)
                              else EVY ((st,q',tacs)::trail, tacs) st
 in
 
 (* EVERY [tac1,...,tacn]   equals    tac1 THEN ... THEN tacn   *)

 
 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
 fun traced_tac seqf st =
     (suppress_tracing := false;
      Seq.make (fn()=> seqf st
-                         handle TRACE_EXIT st' => Some(st', Seq.empty)));
+                         handle TRACE_EXIT st' => SOME(st', Seq.empty)));
 
 
 (*Deterministic DO..UNTIL: only retains the first outcome; tail recursive.
   Forces repitition until predicate on state is fulfilled.*)
 fun DETERM_UNTIL p tac =
 let val tac = tracify trace_REPEAT tac
-    fun drep st = if p st then Some (st, Seq.empty)
+    fun drep st = if p st then SOME (st, Seq.empty)
                           else (case Seq.pull(tac st) of
-                                  None        => None
-                                | Some(st',_) => drep st')
+                                  NONE        => NONE
+                                | SOME(st',_) => drep st')
 in  traced_tac drep  end;
 
 (*Deterministic REPEAT: only retains the first outcome;
   uses less space than REPEAT; tail recursive.
   If non-negative, n bounds the number of repetitions.*)
 fun REPEAT_DETERM_N n tac =
   let val tac = tracify trace_REPEAT tac
-      fun drep 0 st = Some(st, Seq.empty)
+      fun drep 0 st = SOME(st, Seq.empty)
         | drep n st =
            (case Seq.pull(tac st) of
-                None       => Some(st, Seq.empty)
-              | Some(st',_) => drep (n-1) st')
+                NONE       => SOME(st, Seq.empty)
+              | SOME(st',_) => drep (n-1) st')
   in  traced_tac (drep n)  end;
 
 (*Allows any number of repetitions*)
 val REPEAT_DETERM = REPEAT_DETERM_N ~1;
 
 (*General REPEAT: maintains a stack of alternatives; tail recursive*)
 fun REPEAT tac =
   let val tac = tracify trace_REPEAT tac
       fun rep qs st =
         case Seq.pull(tac st) of
-            None       => Some(st, Seq.make(fn()=> repq qs))
-          | Some(st',q) => rep (q::qs) st'
-      and repq [] = None
+            NONE       => SOME(st, Seq.make(fn()=> repq qs))
+          | SOME(st',q) => rep (q::qs) st'
+      and repq [] = NONE
         | repq(q::qs) = case Seq.pull q of
-            None       => repq qs
-          | Some(st,q) => rep (q::qs) st
+            NONE       => repq qs
+          | SOME(st,q) => rep (q::qs) st
   in  traced_tac (rep [])  end;
 
 (*Repeat 1 or more times*)
 fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac;
 fun REPEAT1 tac = tac THEN REPEAT tac;