# HG changeset patch
# User dixon
# Date 1169030372 -3600
# Node ID fd2b69c2f15d47f2372b0bc271959df9fddb3dd7
# Parent  7bf8868ab3e436447dbb0fb9d4e4b0856d67e157
correctled left/right following of another context in zipto.

diff -r 7bf8868ab3e4 -r fd2b69c2f15d src/Provers/IsaPlanner/zipper.ML
--- a/src/Provers/IsaPlanner/zipper.ML	Wed Jan 17 09:53:50 2007 +0100
+++ b/src/Provers/IsaPlanner/zipper.ML	Wed Jan 17 11:39:32 2007 +0100
@@ -332,7 +332,7 @@
   val zipto = 
       C.fold (fn C.D.Abs _ => move_down_abs 
                | C.D.AppL _ => move_down_right
-               | C.D.AppR _ => move_down_left);
+               | C.D.AppR _ => move_down_left); 
 
   (* Note: interpretted as being examined depth first *)
   datatype zsearch = Here of T | LookIn of T;