anchor.diff:  
   /// Apply a higher-order instantiation to a term.
   let instantiate : instantiation -> term -> Choice<term, exn> = 
  -    let betas n tm = 
  -        ([], tm)
  -        |> funpow n (fun (l, t) ->
  -            let rand_t = Choice.get <| rand t
  -            let rator_t = Choice.get <| rator t
  -            rand_t :: l, rator_t)
  -        ||> rev_itlist (fun a l ->
  -            let v, b = Choice.get <| dest_abs l
  -            Choice.get <| vsubst [a, v] b)
  -
  -    let rec ho_betas bcs pat tm = 
  +    let betas n tm =
  +        choice {
  +        // CLEAN : Rename this value to something sensible.
  +        let! foo1 =
  +            ([], tm)
  +            |> Choice.funpow n (fun (l, t) ->
  +                choice {
  +                let! rand_t = rand t
  +                let! rator_t = rator t
  +                return rand_t :: l, rator_t
  +                })
  +        
  +        return
  +            foo1
  +            // TODO : Modify this to use Choice.List.fold.
  +            ||> rev_itlist (fun a l ->
  +                choice {
  +                let! v, b = dest_abs l
  +                return! vsubst [a, v] b
  +                }
  +                |> Choice.get)
  +        }
  +
  +    let rec ho_betas bcs pat tm =
           if is_var pat || is_const pat then
  -            fail()
  -        else 
  -            try 
  -                let bv, bod = Choice.get <| dest_abs tm
  -                let body_pat = Choice.get <| body pat
  -                Choice.get <| mk_abs(bv, ho_betas bcs body_pat bod)
  -            with
  -            | Failure _ -> 
  +            Choice.fail ()
  +        else
  +            choice {
  +            let! bv, bod = dest_abs tm
  +            let! body_pat = body pat
  +            // CLEAN : Rename this value to something sensible.
  +            let! foo1 = ho_betas bcs body_pat bod
  +            return! mk_abs(bv, foo1)
  +            }
  +            |> Choice.bindError (fun _ ->
                   let hop, args = strip_comb pat
                   match rev_assoc hop bcs with
                   | Some n when length args = n ->
                       betas n tm
                   | _ ->
  -                    let lpat, rpat = Choice.get <| dest_comb pat
  -                    let ltm, rtm = Choice.get <| dest_comb tm
  -                    try 
  -                        let lth = ho_betas bcs lpat ltm
  -                        try 
  -                            let rth = ho_betas bcs rpat rtm
  -                            Choice.get <| mk_comb(lth, rth)
  -                        with
  -                        | Failure _ -> Choice.get <| mk_comb(lth, rtm)
  -                    with
  -                    | Failure _ -> 
  -                        let rth = ho_betas bcs rpat rtm
  -                        Choice.get <| mk_comb(ltm, rth)
  +                    // CLEAN : This should be reworked to simplify the code.
  +                    match dest_comb pat with
  +                    | Error error ->
  +                        Choice.error error
  +                    | Success (lpat, rpat) ->
  +                        match dest_comb tm with
  +                        | Error error ->
  +                            Choice.error error
  +                        | Success (ltm, rtm) ->
  +                            match ho_betas bcs lpat ltm with
  +                            | Success lth ->
  +                                match ho_betas bcs rpat rtm with
  +                                | Success rth ->
  +                                    mk_comb(lth, rth)
  +                                | Error _ ->
  +                                    mk_comb(lth, rtm)
  +                            | Error _ ->
  +                                match ho_betas bcs rpat rtm with
  +                                | Success rth ->
  +                                    mk_comb(ltm, rth)
  +                                | Error error ->
  +                                    Choice.error error)
   
       fun (bcs, tmin, tyin) tm ->
  -        Choice.attempt <| fun () ->
  -            let itm = 
  -                if tyin = [] then tm
  -                else Choice.get <| inst tyin tm
  -            if tmin = [] then itm
  -            else 
  -                let ttm = Choice.get <| vsubst tmin itm
  -                if bcs = [] then ttm
  -                else 
  -                    try 
  -                        ho_betas bcs itm ttm
  -                    with
  -                    | Failure _ -> ttm
  +        choice {
  +        let! itm =
  +            choice {
  +            if List.isEmpty tyin then
  +                return tm
  +            else
  +                return! inst tyin tm }
  +
  +        if List.isEmpty tmin then
  +            return itm
  +        else
  +            let! ttm = vsubst tmin itm
  +            if List.isEmpty bcs then
  +                return ttm
  +            else
  +                return!
  +                    ho_betas bcs itm ttm
  +                    |> Choice.bindError (fun _ ->
  +                        Choice.result ttm)
  +        }
   
   /// Apply a higher-order instantiation to conclusion of a theorem.
   let INSTANTIATE : instantiation -> thm -> thm = 
  
positive.code:             |> Choice.bindError (fun _ ->
                  Choice.result tm))
      
      fun env tm ->
          deep_alpha env tm
          |> ExtCore.Choice.bindOrRaise
  
  (* ------------------------------------------------------------------------- *)
  (* Instantiate theorem by matching part of it to a term.                     *)
  
negative.code:             choice {
                  let! (sth, bod, pbod, lconsts, fvs) = v
                  let bvms = match_bvs tm pbod []
                  let! abod = deep_alpha bvms bod
                  let ath = EQ_MP (ALPHA bod abod) sth
                  let! tm1 = partfn abod
                  let! insts = term_match lconsts tm1 tm
  