author | dixon |
Wed, 17 Jan 2007 11:39:32 +0100 | |
changeset 22081 | fd2b69c2f15d |
parent 22080 | 7bf8868ab3e4 |
child 22082 | b1be13d32efd |
--- 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;