anchor.diff:  (* ------------------------------------------------------------------------- *)
   
   /// Applies constant to list of arguments, instantiating constant type as needed.
  -let list_mk_icomb cname args = 
  +let list_mk_icomb cname args : Choice<term, exn> = 
       let list_mk_icomb cname args = 
           let atys, _ = nsplit (Choice.get << dest_fun_ty) args (Choice.get <| get_const_type cname)
           let tyin = itlist2 (fun g a -> Choice.get << type_match g (Choice.get <| type_of a)) atys args []
  
positive.code: (* ------------------------------------------------------------------------- *)
  
  /// Computes a type instantiation to match one type to another.
  let type_match vty cty sofar = 
      let rec type_match vty cty sofar = 
          if is_vartype vty then
              match rev_assoc vty sofar with
              | Some x ->
                  if x = cty then
                      Choice.result sofar
                  else Choice.failwith "type_match"
              | None ->
                  Choice.result <| (cty, vty) :: sofar
          else 
              let vop, vargs = Choice.get <| dest_type vty
              let cop, cargs = Choice.get <| dest_type cty
              if vop = cop then
                  // TODO : Change to use Choice.List.foldBack2 from ExtCore.
                  itlist2 (fun x y z -> Choice.get <| type_match x y z) vargs cargs sofar
                  |> Choice.result
              else Choice.failwith "type_match"
  
      Choice.attemptNested <| fun () ->
          type_match vty cty sofar
  
  (* ------------------------------------------------------------------------- *)
  (* Conventional matching version of mk_const (but with a sanity test).       *)
  
negative.code:         let! mat = type_match uty ty []
          let! con = mk_const(c, mat)
          let! tc = type_of con
          if tc = ty then
              return con
          else
              return! Choice.fail()
      }
      |> Choice.mapError (fun e ->
          nestedFailure e "mk_const: generic type cannot be instantiated")
  