# HG changeset patch
# User dixon
# Date 1162474038 -3600
# Node ID 87a03f9b7db2df3802b5b9ba2aecfca29587831c
# Parent  17b0b4c6491bfb0b6ddf314f290f8bde8987f4d0
bugfix to zipto: left and right were wrong way around.

diff -r 17b0b4c6491b -r 87a03f9b7db2 src/Provers/IsaPlanner/zipper.ML
--- a/src/Provers/IsaPlanner/zipper.ML	Thu Nov 02 13:35:09 2006 +0100
+++ b/src/Provers/IsaPlanner/zipper.ML	Thu Nov 02 14:27:18 2006 +0100
@@ -331,8 +331,8 @@
   (* implicit arguments: C.D.dtrm list, then T *)
   val zipto = 
       C.fold (fn C.D.Abs _ => move_down_abs 
-               | C.D.AppL _ => move_down_left
-               | C.D.AppR _ => move_down_right) 
+               | C.D.AppL _ => move_down_right
+               | C.D.AppR _ => move_down_left);
 
   (* Note: interpretted as being examined depth first *)
   datatype zsearch = Here of T | LookIn of T;