src/Provers/IsaPlanner/zipper.ML

           | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
           | lzyl ((LookIn z) :: more) () =
             (case lzy z
               of NONE => NONE
                | SOME (hz,mz) => 
-                 SOME (hz, Seq.append (mz, Seq.make (lzyl more))))
+                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
         and lzy z = lzyl (fsearch z) ()
       in Seq.make o lzyl o fsearch end;
 
   (* path folded lazy search - the search list is defined in terms of
   the path passed through: the data a is updated with every zipper

         fun lzyl a [] () = NONE
           | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))
           | lzyl a ((LookIn z) :: more) () =
             (case lzy a z
               of NONE => lzyl a more ()
-               | SOME(hz,mz) => SOME(hz,Seq.append(mz,Seq.make(lzyl a more))))
+               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
         and lzy a z = 
             let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
 
         val (a,slist) = fsearch a0 z
       in Seq.make (lzyl a slist) end;

           | lzyl ((a, Here z) :: more) () = 
             SOME((a,z), Seq.make (lzyl more))
           | lzyl ((a, LookIn z) :: more) () =
             (case lzyl (fsearch a z) () of 
                NONE => lzyl more ()
-             | SOME (z,mz) => SOME (z,Seq.append(mz, Seq.make (lzyl more))))
+             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
       in Seq.make (lzyl (fsearch a0 z)) end;
 
 
   fun limit_pcapply f z = 
       let val (z2,c) = split z