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.

--- 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 *)