anchor.diff:  
   let top_goal() =
     let asl,w = top_realgoal() in
  -  map (concl o snd) asl,w;;
  +  map (concl << snd) asl,w;;
   
   let top_thm() =
     let (_,[],f)::_ = !current_goalstack in
  
positive.code:     fun tac1 tac2 g ->
        let _,gls,_ as gstate = tac1 g in
        tacsequence gstate (replicate tac2 (length gls))
    and (thenl_: tactic -> tactic list -> tactic) =
      fun tac1 tac2l g ->
        let _,gls,_ as gstate = tac1 g in
        if gls = [] then tacsequence gstate []
  
negative.code: 
  let (print_goal:goal->unit) =
    let string_of_int3 n =
      if n < 10 then "  " + string_of_int n
      else if n < 100 then " " + string_of_int n
      else string_of_int n in
    let print_hyp n (s,th) =
      Format.open_hbox();
      Format.print_string(string_of_int3 n);
      Format.print_string " [";
      Format.open_hvbox 0;
      print_qterm (concl th);
      Format.close_box();
      Format.print_string "]";
      (if not (s = "") then (Format.print_string (" (" + s + ")")) else ());
      Format.close_box();
      Format.print_newline() in
    let rec print_hyps n asl =
      if asl = [] then () else
  