anchor.diff:  (* ------------------------------------------------------------------------- *)
   
   /// Parses a string into a HOL type.
  -let parse_type (s : string) =
  +let parse_type s =
   //    printfn "parsing type %s" s 
       let pty, l = (parse_pretype << lex << explode) s
       //printfn "pty, l <-- %A, %A" pty l
       if l = [] then Choice.get <| type_of_pretype pty
       else failwith "Unparsed input following type"
  +
  +let tryParseType s =
  +    try
  +        Choice.succeed <| parse_type s
  +    with
  +    | :? Noparse ->
  +        Choice.failwith "Noparse"
  +    | Failure s ->
  +        Choice.failwith s
   
   /// Parses a string into a HOL term.
   let parse_term s = 
  
positive.code:       if length fvs <= 1 || bvs = [] then fvs
        else intersect fvs bvs
      pmk_setcompr (fabs,evs,babs)
    let rec mk_precedence infxs prs inp =
      match infxs with
        (s,(p,at))::_ ->
  
negative.code:             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 -> 
          match remove (fun (key', _) -> key = key') (!parser_list) with
          | Some (_, p) -> parser_list := p
          | None -> ()), 
      (fun () -> !parser_list), 
      (fun i -> try_parsers (!parser_list) i)
  
  (* ------------------------------------------------------------------------- *)
  (* Initial preterm parsing. This uses binder and precedence/associativity/   *)
  