anchor.diff:  (* ------------------------------------------------------------------------- *)
   
   /// Determines which binary operators are line-broken to the left.
  -let prebroken_binops = ref ["==>"]
  +let prebroken_binops =
  +    ref ["==>"]
   
   (* ------------------------------------------------------------------------- *)
   (* Force explicit indications of bound variables in set abstractions.        *)
  
positive.code: (* Printer for types.                                                        *)
  (* ------------------------------------------------------------------------- *)
  
  // pp_print_type: Prints a type (without colon or quotes) to formatter.
  // pp_print_qtype: Prints a type with initial colon and surrounding quotes to formatter.
  let pp_print_type, pp_print_qtype = 
      let soc sep flag ss = 
          if ss = [] then ""
          else 
              let s = end_itlist (fun s1 s2 -> s1 + sep + s2) ss
              if flag then "(" + s + ")"
              else s
      let rec sot pr ty = 
          match dest_vartype ty with
          | Success s -> s
          | Error _ -> 
              match dest_type ty with
              | Success ty' ->
                  match ty' with
                  | con, [] -> con
                  | "fun", [ty1; ty2] -> 
                      soc "->" (pr > 0) [sot 1 ty1;
                                         sot 0 ty2]
                  | "sum", [ty1; ty2] -> 
                      soc "+" (pr > 2) [sot 3 ty1;
                                        sot 2 ty2]
                  | "prod", [ty1; ty2] -> 
                      soc "#" (pr > 4) [sot 5 ty1;
                                        sot 4 ty2]
                  | "cart", [ty1; ty2] -> 
                      soc "^" (pr > 6) [sot 6 ty1;
                                        sot 7 ty2]
                  | con, args -> (soc "," true (map (sot 0) args)) + con
              | Error _ -> "malformed type"
      (fun fmt ty -> pp_print_string fmt (sot 0 ty)), (fun fmt ty -> pp_print_string fmt ("`:" + sot 0 ty + "`"))
  
  (* ------------------------------------------------------------------------- *)
  (* Allow the installation of user printers. Must fail quickly if N/A.        *)
  (* ------------------------------------------------------------------------- *)
  
  // install_user_printer: Install a user-defined printing function into the HOL Light term printer.
  // delete_user_printer: Remove user-defined printer from the HOL Light term printing.
  // try_user_printer: Try user-defined printers on a term.
  let install_user_printer, delete_user_printer, (try_user_printer : term -> Protected<unit>) = 
      let user_printers = ref([] : (string * (term -> unit)) list)
      (fun pr ->
          user_printers := pr :: !user_printers), 
      (fun s ->
          user_printers := snd(Option.get <| remove (fun (s', _) -> s = s') !user_printers)),
      (fun tm ->
          !user_printers
          |> tryfind (fun (_, pr) ->
              // NOTE: wrong use of Some, need to change this
              Some <| pr tm)
          |> Option.toChoiceWithError "find")
  
  (* ------------------------------------------------------------------------- *)
  (* Printer for terms.                                                        *)
  
negative.code: (* Character discrimination.                                                 *)
  (* ------------------------------------------------------------------------- *)
  
  let inline private charcode (s : string) =
      int s.[0]
  
  let private ctable =
      let spaces = " \t\n\r"
      let separators = ",;"
      let brackets = "()[]{}"
  