anchor.diff:  
   // https://github.com/gilith/hol-light/blob/master/Help/parse_as_infix.doc
   // parse_as_infix : string * (int * string) -> unit
  -parse_as_infix (",",(14,"right"))
  +parse_as_infix(",", (14, "right"))
   
   (* ------------------------------------------------------------------------- *)
   (* Basic parser combinators.                                                 *)
  
positive.code: (* Type and term parsers.                                                    *)
  (* ------------------------------------------------------------------------- *)
  
  let parse_type s =
    let pty,l = (parse_pretype << lex << explode) s
    if l = [] then type_of_pretype pty
    else failwith "Unparsed input following type"
  
  let parse_term s =
    let ptm,l = (parse_preterm << lex << explode) s
    if l = [] then (term_of_preterm << (retypecheck [])) ptm
    else failwith "Unparsed input following term"
  
  
  
negative.code: (*  o Antiquotation is not supported.                                        *)
  (* ------------------------------------------------------------------------- *)
  
  let parse_pretype = 
      let btyop n n' x y = Ptycon(n, [x; y])
      let mk_apptype = 
          function 
          | [s], [] -> s
          | tys, [c] -> Ptycon(c, tys)
          | _ -> failwith "Bad type construction"
      let type_atom input = 
          match input with
          | (Ident s) :: rest -> 
              let result = 
                  try 
                      pretype_of_type(assoc s (type_abbrevs()))
                  with
                  | Failure _ -> 
                      if (try 
                              get_type_arity s = 0
                          with
                          | Failure _ -> false)
                      then Ptycon(s, [])
                      else Utv(s)
              result, rest
          | _ -> raise Noparse
      let type_constructor input = 
          match input with
          | (Ident s) :: rest -> 
              if (try 
                      get_type_arity s > 0
                  with
                  | Failure _ -> false)
              then s, rest
              else raise Noparse
          | _ -> raise Noparse
      let rec pretype i = rightbin sumtype (a(Resword "->")) (btyop "fun") "type" i
      and sumtype i = rightbin prodtype (a(Ident "+")) (btyop "sum") "type" i
      and prodtype i = rightbin carttype (a(Ident "#")) (btyop "prod") "type" i
      and carttype i = leftbin apptype (a(Ident "^")) (btyop "cart") "type" i
      and apptype i = (atomictypes .>>. (type_constructor |>> (fun x -> [x]) <|> nothing) |>> mk_apptype) i
      and atomictypes i = 
          (((a(Resword "(")) .>>. typelist .>>. (a(Resword ")")) |>> (snd << fst)) <|> (type_atom |>> (fun x -> [x]))) i
      and typelist i = (listof pretype (a(Ident ",")) "type") i
      pretype
  
  (* ------------------------------------------------------------------------- *)
  (* Hook to allow installation of user parsers.                               *)
  (* ------------------------------------------------------------------------- *)
  
  let install_parser, delete_parser, installed_parsers, try_user_parser = 
      let rec try_parsers ps i = 
          match ps with
          | [] -> raise Noparse
          | hd :: tl -> 
              try 
                  (snd hd) i
              with
              | Noparse -> try_parsers tl i
      let parser_list = ref([] : (string * (lexcode list -> preterm * lexcode list)) list)
      (fun dat -> parser_list := dat :: (!parser_list)), (fun key -> 
          try 
              parser_list := snd(remove (fun (key', _) -> key = key') (!parser_list))
          with
          | Failure _ -> ()), (fun () -> !parser_list), (fun i -> try_parsers (!parser_list) i)
  
  (* ------------------------------------------------------------------------- *)
  (* Initial preterm parsing. This uses binder and precedence/associativity/   *)
  