src/Provers/IsaPlanner/zipper.ML
changeset 19861 620d90091788
parent 19853 cb73c3c367db
child 19871 88e8f6173bab
     1.1 --- a/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/Provers/IsaPlanner/zipper.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -321,7 +321,7 @@
     1.4              (case lzy z
     1.5                of NONE => NONE
     1.6                 | SOME (hz,mz) => 
     1.7 -                 SOME (hz, Seq.append (mz, Seq.make (lzyl more))))
     1.8 +                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
     1.9          and lzy z = lzyl (fsearch z) ()
    1.10        in Seq.make o lzyl o fsearch end;
    1.11  
    1.12 @@ -335,7 +335,7 @@
    1.13            | lzyl a ((LookIn z) :: more) () =
    1.14              (case lzy a z
    1.15                of NONE => lzyl a more ()
    1.16 -               | SOME(hz,mz) => SOME(hz,Seq.append(mz,Seq.make(lzyl a more))))
    1.17 +               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
    1.18          and lzy a z = 
    1.19              let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
    1.20  
    1.21 @@ -351,7 +351,7 @@
    1.22            | lzyl ((a, LookIn z) :: more) () =
    1.23              (case lzyl (fsearch a z) () of 
    1.24                 NONE => lzyl more ()
    1.25 -             | SOME (z,mz) => SOME (z,Seq.append(mz, Seq.make (lzyl more))))
    1.26 +             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
    1.27        in Seq.make (lzyl (fsearch a0 z)) end;
    1.28  
    1.29