anchor.diff:              }
               |> Choice.bindError (fun _ ->
                   let hop, args = strip_comb pat
  -                let v = 
  -                    rev_assoc hop bcs
  -                    |> Option.toChoiceWithError "find"
  -                    |> Choice.bind (fun n ->
  -                        if length args = n
  -                        then BETAS_CONV n tm
  -                        else Choice.fail ())
  -                v |> Choice.bindError (fun _ -> 
  +                rev_assoc hop bcs
  +                |> Option.toChoiceWithError "find"
  +                |> Choice.bind (fun n ->
  +                    if length args = n then
  +                        BETAS_CONV n tm
  +                    else
  +                        Choice.fail ())
  +                |> Choice.bindError (fun _ ->
                       choice {
                           let! lpat, rpat = dest_comb pat
                           let! ltm, rtm = dest_comb tm
                           
  -                        let lth = HO_BETAS bcs lpat ltm
  -                        let v' = 
  -                            let rth = HO_BETAS bcs rpat rtm
  +                        let! lth = HO_BETAS bcs lpat ltm
  +                        let! rth = HO_BETAS bcs rpat rtm
  +                        return!
  +                            let lth = Choice.result lth in
  +                            let rth = Choice.result rth in
                               MK_COMB(lth, rth)
  -                        return! v' |> Choice.bindError (fun _ -> AP_THM lth rtm)
  -                                   |> Choice.bindError (fun _ -> 
  -                                        let rth = HO_BETAS bcs rpat rtm
  -                                        AP_TERM ltm rth)
  +                            |> Choice.bindError (fun _ ->
  +                                AP_THM lth rtm)
  +                            |> Choice.bindError (fun _ ->
  +                                choice {
  +                                let! rth = HO_BETAS bcs rpat rtm
  +                                return! AP_TERM ltm (Choice.result rth)
  +                                })
                       }))
   
  -    fun (bcs, tmin, tyin) th -> 
  -        let ith = 
  -            if tyin = [] then th
  -            else INST_TYPE tyin th
  -        if tmin = [] then ith
  +    fun (bcs, tmin, tyin) th ->
  +        choice {
  +        let! th = th
  +        let! ith =
  +            choice {
  +            if List.isEmpty tyin then
  +                return th
  +            else
  +                return! INST_TYPE tyin (Choice.result th) }
  +
  +        if List.isEmpty tmin then
  +            return ith
           else
  -            choice { 
  -                let tth = INST tmin ith
  -                let! tl1 = Choice.map hyp tth
  -                let! tl2 = Choice.map hyp th
  -                if tl1 = tl2 then 
  -                    if bcs = [] then 
  -                        return! tth
  -                    else 
  -                        let! itm = Choice.map concl ith
  -                        let! ttm = Choice.map concl tth
  -                        let v = 
  -                            let eth = HO_BETAS bcs itm ttm
  -                            EQ_MP eth tth
  -                        return! v |> Choice.bindError (fun _ -> tth)
  -                else 
  -                    return! Choice.failwith "INSTANTIATE: term or type var free in assumptions"
  -            }
  +            let! tth = INST tmin (Choice.result ith)
  +            let tl1 = hyp tth
  +            let tl2 = hyp th
  +
  +            if tl1 = tl2 then
  +                if List.isEmpty bcs then
  +                    return tth
  +                else
  +                    let itm = concl ith
  +                    let ttm = concl tth
  +                    let! eth = HO_BETAS bcs itm ttm
  +                    return!
  +                        let eth = Choice.result eth in
  +                        let tth = Choice.result tth in
  +                        EQ_MP eth tth
  +                        |> Choice.bindError (fun _ -> tth)
  +            else 
  +                return! Choice.failwith "INSTANTIATE: term or type var free in assumptions"
  +        }
   
   /// Apply a higher-order instantiation to assumptions and conclusion of a theorem.
  -let INSTANTIATE_ALL : instantiation -> thm -> thm = 
  +let INSTANTIATE_ALL : instantiation -> thm -> thm =
       let inst ((_, tmin, tyin) as i) th =
  -        if tmin = [] && tyin = [] then th
  -        else 
  -            let hyps = hyp <| Choice.get th
  -            if hyps = [] then INSTANTIATE i th
  -            else 
  -                let tyrel, tyiirel = 
  -                    if tyin = [] then [], hyps
  -                    else 
  +        choice {
  +        let! th = th
  +        if List.isEmpty tmin && List.isEmpty tyin then
  +            return th
  +        else
  +            let hyps = hyp th
  +            if List.isEmpty hyps then
  +                return! INSTANTIATE i (Choice.result th)
  +            else
  +                let! tyrel, tyiirel =
  +                    if List.isEmpty tyin then
  +                        Choice.result ([], hyps)
  +                    else
                           let tvs = itlist (union << tyvars << snd) tyin []
  -                        partition (fun tm -> 
  -                                let tvs' = Choice.get <| type_vars_in_term tm
  -                                not(intersect tvs tvs' = [])) hyps
  -                let tmrel, tmirrel = 
  -                    if tmin = [] then
  +                        hyps
  +                        // TODO : Modify this to use Choice.List.partition.
  +                        |> Choice.List.partition (fun tm ->
  +                            choice {
  +                            let! tvs' = type_vars_in_term tm
  +                            return not(intersect tvs tvs' = [])
  +                            })
  +                
  +                let tmrel, tmirrel =
  +                    if List.isEmpty tmin then
                           [], tyiirel
  -                    else 
  +                    else
                           let vs = itlist (union << frees << snd) tmin []
  -                        partition (fun tm -> 
  -                                let vs' = frees tm
  -                                not(intersect vs vs' = [])) tyiirel
  +                        tyiirel
  +                        |> partition (fun tm ->
  +                            let vs' = frees tm
  +                            not(intersect vs vs' = []))
  +                
                   let rhyps = union tyrel tmrel
  -                let th1 = rev_itlist DISCH rhyps th
  -                let th2 = INSTANTIATE i th1
  -                funpow (length rhyps) UNDISCH th2
  -    fun i th ->
  -        Choice.attemptNested <| fun () ->
  -            inst i th
  +                let! th1 =
  +                    // TODO : Modify this to use Choice.List.fold/foldBack.
  +                    rev_itlist DISCH rhyps (Choice.result th)
  +                let! th2 = INSTANTIATE i (Choice.result th1)
  +                return! funpow (length rhyps) UNDISCH (Choice.result th2)
  +        }
  +    
  +    inst
   
   (* ------------------------------------------------------------------------- *)
   (* Higher order matching of terms.                                           *)
  
positive.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
  
negative.code: (* ------------------------------------------------------------------------- *)
  
  /// Modify bound variable according to renaming scheme.
  let deep_alpha : (string * string) list -> term -> Protected<term> = 
      let tryalpha v tm =
          match alpha v tm with
          | Success x -> x
  