anchor.diff:  
   /// Applies a conversion to both arguments of a binary operator.
   let BINOP_CONV conv tm = 
  -    let lop, r = Choice.get <| dest_comb tm
  -    let op, l = Choice.get <| dest_comb lop
  -    MK_COMB(AP_TERM op (conv l), conv r)
  +    choice {
  +        let! lop, r = dest_comb tm
  +        let! op, l = dest_comb lop
  +        return! MK_COMB(AP_TERM op (conv l), conv r)
  +    }
   
   (* ------------------------------------------------------------------------- *)
   (* Depth conversions; internal use of a failure-propagating `Boultonized'    *)
  
positive.code: /// Applies two conversions in sequence.
  let THENC : conv -> conv -> conv = 
      fun conv1 conv2 t -> 
          let th1 = conv1 t
          let th2 = conv2 (Choice.get <| rand(concl <| Choice.get th1))
          TRANS th1 th2
  
  /// Applies the first of two conversions that succeeds.
  let ORELSEC : conv -> conv -> conv = 
  
negative.code:         |> Choice.bindError (fun _ -> conv2 t)
  
  /// Apply the first of the conversions in a given list that succeeds.
  let FIRST_CONV : conv list -> conv = 
      end_itlist ORELSEC
  
  /// Applies in sequence all the conversions in a given list of conversions.
  let EVERY_CONV : conv list -> conv = fun l -> itlist THENC l ALL_CONV
  