anchor.diff:                                        (parse_term @"x pow n"), REAL_RAT_POW_CONV;
                                         (parse_term @"max x y"), REAL_RAT_MAX_CONV;
                                         (parse_term @"min x y"), REAL_RAT_MIN_CONV] 
  -            (basic_net())
  -    REWRITES_CONV gconv_net
  +    
  +    // NOTE: add this argument to propagate errors
  +    fun tm ->   
  +        choice {    
  +            let! gconv_net = gconv_net
  +            return! REWRITES_CONV gconv_net tm
  +        }
   
   /// Evaluate subexpressions built up from rational literals of type :real, by proof.
   let REAL_RAT_REDUCE_CONV = DEPTH_CONV REAL_RAT_RED_CONV
  
positive.code:                   |> THEN <| ASM_REWRITE_TAC []
                    DISCH_THEN(fun th -> ASM_REWRITE_TAC [MATCH_MP RAT_LEMMA5 th])])
  
    let dest_divop = Choice.get << dest_binop(parse_term @"(/)")
    let dest_addop = Choice.get << dest_binop(parse_term @"(+)")
    let x1 = (parse_term @"x1:real")
    let x2 = (parse_term @"x2:real")
    let x3 = (parse_term @"x3:real")
  
negative.code:     let x2 = (parse_term @"x2:real")
      let y1 = (parse_term @"y1:real")
      let y2 = (parse_term @"y2:real")
      let dest_le = dest_binop(parse_term @"(<=)")
      let dest_div = dest_binop(parse_term @"(/)")
      let RAW_REAL_RAT_LE_CONV tm = 
          choice {
              let! l, r = dest_le tm
              let! lx, ly = dest_div l
              let! rx, ry = dest_div r
              let th0 = 
                  INST [lx, x1;
                        ly, y1;
                        rx, x2;
                        ry, y2] pth
              let! th1 = funpow 2 (MP_CONV REAL_INT_LT_CONV) th0
              let! tm1 = rand(concl th1)
              let th2 = (BINOP_CONV REAL_INT_MUL_CONV
                         |> THENC <| REAL_INT_LE_CONV) tm1
              return! TRANS (Choice.result th1) th2
          }
  
      BINOP_CONV REAL_INT_RAT_CONV
      |> THENC <| RAW_REAL_RAT_LE_CONV
  
  