src/Pure/tctical.ML

 (*passes no proofs through;  identity of ORELSE and APPEND*)
 fun no_tac st  = Seq.empty;
 
 
 (*Make a tactic deterministic by chopping the tail of the proof sequence*)
-fun DETERM tac st =  
-      case Seq.pull (tac st) of
-              None => Seq.empty
-            | Some(x,_) => Seq.cons(x, Seq.empty);
-
+fun DETERM tac = Seq.DETERM tac;
 
 (*Conditional tactical: testfun controls which tactic to use next.
   Beware: due to eager evaluation, both thentac and elsetac are evaluated.*)
 fun COND testfun thenf elsef = (fn prf =>
     if testfun prf then  thenf prf   else  elsef prf);