anchor.diff:  /// Applies two conversions to the two sides of an application.
   let COMB2_CONV : conv -> conv -> conv = 
       fun lconv rconv tm -> 
  -        let l, r = Choice.get <| dest_comb tm
  -        MK_COMB(lconv l, rconv r)
  +        dest_comb tm
  +        |> Choice.bind (fun (l, r) ->
  +            MK_COMB(lconv l, rconv r))
   
   /// Applies a conversion to the two sides of an application.
   let COMB_CONV = W COMB2_CONV
   
  -/// Applies a conversion to the Choice.get <| body of an abstraction.
  +/// Applies a conversion to the body of an abstraction.
   let ABS_CONV : conv -> conv = 
       fun conv tm -> 
  -        let v, bod = Choice.get <| dest_abs tm
  -        let th = conv bod
  -        ABS v th
  -        |> Choice.bindError(fun _ ->
  -            let gv = genvar(Choice.get <| type_of v)
  -            let gbod = Choice.get <| vsubst [gv, v] bod
  -            let gth = ABS gv (conv gbod)
  -            let gtm = concl <| Choice.get gth
  -            let l, r = Choice.get <| dest_eq gtm
  -            let v' = Choice.get <| variant (frees gtm) v
  -            let l' = Choice.get <| alpha v' l
  -            let r' = Choice.get <| alpha v' r
  -            EQ_MP (ALPHA gtm (Choice.get <| mk_eq(l', r'))) gth)
  -
  -/// Applies conversion to the Choice.get <| body of a binder.
  +        choice {
  +            let! v, bod = dest_abs tm
  +            let th = conv bod
  +            return! ABS v th
  +            |> Choice.bindError(fun _ ->
  +                choice {
  +                    let! tv = type_of v
  +                    let gv = genvar tv
  +                    let! gbod = vsubst [gv, v] bod
  +                    let gth = ABS gv (conv gbod)
  +                    let! gtm = Choice.map concl gth
  +                    let! l, r = dest_eq gtm
  +                    let! v' = variant (frees gtm) v
  +                    let! l' = alpha v' l
  +                    let! r' = alpha v' r
  +                    let! tm' = mk_eq(l', r')
  +                    return! EQ_MP (ALPHA gtm tm') gth
  +                })
  +        }
  +
  +/// Applies conversion to the body of a binder.
   let BINDER_CONV conv tm = 
       if is_abs tm then ABS_CONV conv tm
       else RAND_CONV (ABS_CONV conv) tm
  
positive.code: /// Applies a conversion to the operator of an application.
  let RATOR_CONV : conv -> conv = 
      fun conv tm -> 
          let l, r = Choice.get <| dest_comb tm
          AP_THM (conv l) r
  
  /// Applies a conversion to the operand of an application.
  let RAND_CONV : conv -> conv = 
      fun conv tm -> 
          let l, r = Choice.get <| dest_comb tm
          AP_TERM l (conv r)
  
  /// Apply a conversion to left-hand argument of binary operator.
  let LAND_CONV = RATOR_CONV << RAND_CONV
  
negative.code: /// Makes a conversion fail if applying it leaves a term unchanged.
  let CHANGED_CONV : conv -> conv = 
      fun conv tm -> 
          choice {
              let th = conv tm
              let! l, r = Choice.bind (dest_eq << concl) th
              if aconv l r then 
                  return! Choice.failwith "CHANGED_CONV"
              else return! th
          }
  
  /// Attempts to apply a conversion; applies identity conversion in case of failure.
  let TRY_CONV conv = ORELSEC conv ALL_CONV
  