src/Pure/IsaPlanner/isaplib.ML

 	    NONE => NONE
 	  | SOME (a, s2) => 
 	    (case Seq.pull s2 of 
 	       NONE => NONE
 	     | SOME (a2,s3) => 
-	       SOME (a, all_but_last_of_seq (Seq.cons (a2,s3))))
+	       SOME (a, all_but_last_of_seq (Seq.cons a2 s3)))
     in
       Seq.make f
     end;
 
  fun ALL_BUT_LAST r st = all_but_last_of_seq (r st);

       fun skip_occs n sq = 
           case Seq.pull sq of 
             NONE => skipmore n
           | SOME (h,t) => 
             (case Seq.pull h of NONE => skip_occs n t
-             | SOME _ => if n <= 1 then skipseq (Seq.cons (h, t))
+             | SOME _ => if n <= 1 then skipseq (Seq.cons h t)
                          else skip_occs (n - 1) t)
     in (skip_occs m s) end;
 
 (* handy function for re-arranging Sequence operations *)
 (* [[a,b,c],[d,e],...] => flatten [[a,d,...], [b,e,...], [c, ...]] *)