anchor.diff:  /// Lexical analyzer, type and preterm parsers.
   module NHol.parser
   
  +open NHol.lib
  +open NHol.preterm
  +
   (*
   
   (* ------------------------------------------------------------------------- *)
   (* Need to have this now for set enums, since "," isn't a reserved word.     *)
   (* ------------------------------------------------------------------------- *)
   
  -parse_as_infix (",",(14,"right"));;
  +// 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"))
   
   (* ------------------------------------------------------------------------- *)
   (* Basic parser combinators.                                                 *)
   (* ------------------------------------------------------------------------- *)
   
  -exception Noparse;;
  +exception Noparse
   
   let (||) parser1 parser2 input =
  -  try parser1 input
  -  with Noparse -> parser2 input;;
  +    try parser1 input
  +    with Noparse -> parser2 input
   
   let (++) parser1 parser2 input =
  -  let result1,rest1 = parser1 input in
  -  let result2,rest2 = parser2 rest1 in
  -  (result1,result2),rest2;;
  +    let result1, rest1 = parser1 input
  +    let result2, rest2 = parser2 rest1
  +    (result1, result2), rest2
   
   let rec many prs input =
  -  try let result,next = prs input in
  -      let results,rest = many prs next in
  -      (result::results),rest
  -  with Noparse -> [],input;;
  +    try
  +        let result, next = prs input
  +        let results, rest = many prs next
  +        (result :: results), rest
  +    with Noparse ->
  +        [],input
   
   let (>>) prs treatment input =
  -  let result,rest = prs input in
  -  treatment(result),rest;;
  +    let result,rest = prs input
  +    treatment result, rest
   
   let fix err prs input =
  -  try prs input
  -  with Noparse -> failwith (err ^ " expected");;
  +    try prs input
  +    with Noparse ->
  +        failwith (err ^ " expected")
   
   let rec listof prs sep err =
  -  prs ++ many (sep ++ fix err prs >> snd) >> (fun (h,t) -> h::t);;
  -
  -let nothing input = [],input;;
  +    prs ++ many (sep ++ fix err prs >> snd) >> (fun (h, t) -> h :: t)
  +
  +let nothing input = [], input
   
   let elistof prs sep err =
  -  listof prs sep err || nothing;;
  +    listof prs sep err || nothing;;
   
   let leftbin prs sep cons err =
  -  prs ++ many (sep ++ fix err prs) >>
  -  (fun (x,opxs) -> let ops,xs = unzip opxs in
  -                   itlist2 (fun op y x -> cons op x y) (rev ops) (rev xs) x);;
  +    prs ++ many (sep ++ fix err prs) >>
  +    (fun (x,opxs) ->
  +        let ops, xs = unzip opxs
  +        itlist2 (fun op y x -> cons op x y) (rev ops) (rev xs) x);;
   
   let rightbin prs sep cons err =
  -  prs ++ many (sep ++ fix err prs) >>
  -  (fun (x,opxs) -> if opxs = [] then x else
  -                   let ops,xs = unzip opxs in
  -                   itlist2 cons ops (x::butlast xs) (last xs));;
  +    prs ++ many (sep ++ fix err prs) >>
  +    (fun (x, opxs) ->
  +        if opxs = [] then x
  +        else
  +            let ops, xs = unzip opxs
  +            itlist2 cons ops (x::butlast xs) (last xs))
   
   let possibly prs input =
  -  try let x,rest = prs input in [x],rest
  -  with Noparse -> [],input;;
  -
  -let some p =
  -  function
  -      [] -> raise Noparse
  -    | (h::t) -> if p h then (h,t) else raise Noparse;;
  -
  -let a tok = some (fun item -> item = tok);;
  +    try
  +        let x, rest = prs input
  +        [x], rest
  +    with Noparse ->
  +        [],input
  +
  +let some p = function
  +    | [] -> raise Noparse
  +    | h :: t ->
  +        if p h then h, t
  +        else raise Noparse
  +
  +let a tok = some (fun item -> item = tok)
   
   let rec atleast n prs i =
  -  (if n <= 0 then many prs
  -   else prs ++ atleast (n - 1) prs >> (fun (h,t) -> h::t)) i;;
  +    (if n <= 0 then many prs
  +     else prs ++ atleast (n - 1) prs >> (fun (h,t) -> h :: t)) i
   
   let finished input =
  -  if input = [] then 0,input else failwith "Unparsed input";;
  +    if input = [] then 0, input
  +    else failwith "Unparsed input"
   
   (* ------------------------------------------------------------------------- *)
   (* The basic lexical classes: identifiers, strings and reserved words.       *)
   (* ------------------------------------------------------------------------- *)
   
  -type lexcode = Ident of string
  -             | Resword of string;;
  +type lexcode =
  +    | Ident of string
  +    | Resword of string
   
   (* ------------------------------------------------------------------------- *)
   (* Lexical analyzer. Apart from some special bracket symbols, each           *)
  
positive.code: (* the longest string of symbolics.                                          *)
  (* ------------------------------------------------------------------------- *)
  
  reserve_words ["//"];;
  
  let comment_token = ref (Resword "//");;
  
  let lex =
    let collect (h,t) = end_itlist (^) (h::t) in
    let reserve =
      function
          (Ident n as tok) ->
              if is_reserved_word n then Resword(n) else tok
        | t -> t in
    let stringof p = atleast 1 p >> end_itlist (^) in
    let simple_ident = stringof(some isalnum) || stringof(some issymb) in
    let undertail = stringof (a "_") ++ possibly simple_ident >> collect in
  
negative.code:   and lmk_setcompr(((((f,_),vs),_),b),_) =
       pmk_setcompr(f,pfrees vs [],b)
    and lmk_decimal ((_,l0),ropt) =
       let l,r = if ropt = [] then l0,"1" else
                let r0 = hd ropt in
                let n_l = num_of_string l0
                let n_r = num_of_string r0
                let n_d = power_num (Int 10) (Int (String.length r0))
                let n_n = n_l */ n_d +/ n_r
                string_of_num n_n,string_of_num n_d
       Combp(Combp(Varp("DECIMAL",dpty),Varp(l,dpty)),Varp(r,dpty))
    and lmk_univ((_,pty),_) =
      Typing(Varp("UNIV",dpty),Ptycon("fun",[pty;Ptycon("bool",[])]))
  