# HG changeset patch # User dixon # Date 1124134705 -7200 # Node ID 94d38d9fac4087aa897b301e43ba06f61ff01867 # Parent d3e52c3bfb076d73653b9805d97097a3134803bb lucas - fixed bug in changing focus - when moving up and right, if an abs was encountered it would move up an extra time. I also removed the spurious pretty printing function that did nothing. diff -r d3e52c3bfb07 -r 94d38d9fac40 src/Pure/IsaPlanner/focus_term_lib.ML --- a/src/Pure/IsaPlanner/focus_term_lib.ML Wed Aug 10 15:29:56 2005 +0200 +++ b/src/Pure/IsaPlanner/focus_term_lib.ML Mon Aug 15 21:38:25 2005 +0200 @@ -122,7 +122,6 @@ (* analysis *) val upsize_of_fcterm : FcTerm -> int - val pretty_fcterm : FcTerm -> Pretty.T end; @@ -293,7 +292,7 @@ fun focus_up_abs_or_appr (focus(t, appl(l,m))) = NONE | focus_up_abs_or_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m)) | focus_up_abs_or_appr (focus(t, abs(s,ty,m))) = - SOME (focus_up (focus(Abs(s,ty,t), m))) + SOME (focus(Abs(s,ty,t), m)) | focus_up_abs_or_appr (focus(t, root)) = NONE; @@ -338,11 +337,8 @@ Seq.cons (botleft, (Seq.make (next_leaf_of_fcterm_seq_aux botleft)) ) end; - fun upsize_of_fcterm (focus(t, ut)) = upsize_of_upterm ut; - fun pretty_fcterm ft = Pretty.str "no yet implemented"; - end; (* local *) end; (* functor *)