src/Provers/IsaPlanner/zipper.ML

--- a/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 21:18:10 2006 +0200
+++ b/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 21:19:00 2006 +0200
@@ -321,7 +321,7 @@
             (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;
 
@@ -335,7 +335,7 @@
           | 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
 
@@ -351,7 +351,7 @@
           | 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;