anchor.diff:          |> 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 (fun c1 c2 -> ORELSEC c1 c2)
  +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
  
positive.code: /// 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)
  
  /// 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.
  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.
  let BINDER_CONV conv tm = 
      if is_abs tm then ABS_CONV conv tm
      else RAND_CONV (ABS_CONV conv) tm
  
negative.code: /// Applies two conversions in sequence.
  let THENC : conv -> conv -> conv = 
      fun conv1 conv2 t -> 
          choice {
              let th1 = conv1 t
              let! t' = Choice.bind (rand << concl) th1
              let th2 = conv2 t'
              return! TRANS th1 th2
          }
  
  /// Applies the first of two conversions that succeeds.
  let ORELSEC : conv -> conv -> conv = 
  