diff -r d3c16021e999 -r e87496286934 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Fri Jan 25 15:42:59 2002 +0100
+++ b/src/Pure/tctical.ML	Sat Jan 26 19:15:51 2002 +0100
@@ -133,11 +133,7 @@
 
 
 (*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.*)