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:     let abs = itlist (fun v t -> Absp(v,t)) vars lend
      let labs = Combp(Varp("LET",dpty),abs)
      rev_itlist (fun x f -> Combp(f,x)) tms labs
    let pmk_vbinder(n,v,bod) =
      if n = "\\" then Absp(v,bod)
      else Combp(Varp(n,dpty),Absp(v,bod))
    let pmk_binder(n,vs,bod) = itlist (fun v b -> pmk_vbinder(n,v,b)) vs bod
    let pmk_set_enum ptms = itlist (fun x t -> Combp(Combp(Varp("INSERT",dpty),x),t)) ptms (Varp("EMPTY",dpty))
    let pgenvar =
      let gcounter = ref 0
      fun () ->
          let count = !gcounter
          gcounter := count + 1
          Varp("GEN%PVAR%"+(string count),dpty)
    let pmk_exists(v,ptm) = Combp(Varp("?",dpty),Absp(v,ptm))
    let pmk_list els = itlist (fun x y -> Combp(Combp(Varp("CONS",dpty),x),y)) els (Varp("NIL",dpty))
    let pmk_bool =
      let tt = Varp("T",dpty)
      let ff = Varp("F",dpty)
      fun b ->
          if b then tt else ff
    let pmk_char c =
      let lis = map (fun i -> pmk_bool((c / (1 <<< i)) % 2 = 1)) (0--7)
      itlist (fun x y -> Combp(y,x)) lis (Varp("ASCII",dpty))
    let pmk_string s =
      let ns = map (fun i -> Char.code(String.get s i)) (0--(String.length s - 1))
      pmk_list(map pmk_char ns)
    let pmk_setcompr (fabs,bvs,babs) =
      let v = pgenvar()
      let bod = itlist (curry pmk_exists) bvs (Combp(Combp(Combp(Varp("SETSPEC",dpty),v),babs),fabs))
      Combp(Varp("GSPEC",dpty),Absp(v,bod))
    let pmk_setabs (fabs,babs) =
      let evs =
        let fvs = pfrees fabs []
  
negative.code:       Combp(Combp(Varp("DECIMAL", dpty), Varp(l, dpty)), Varp(r, dpty))
    
    and lmk_univ((_, pty), _) = 
        Typing(Varp("UNIV", dpty), Ptycon("fun", [pty; Ptycon("bool", [])]))
    
    and any_identifier = 
        function 
  