anchor.diff:          with
           | Failure _ -> 
               let th = conv tm
  -            net := Choice.get <| enter [] (tm, ALPHA_HACK th) (!net)
  +            match enter [] (tm, ALPHA_HACK th) (!net) with
  +            | Success n -> net := n
  +            | Error _ -> 
  +                // NOTE: currently do nothing in case of error
  +                ()
               th
  
positive.code: let SUBS_CONV ths tm = 
      let tm = 
          if ths = [] then REFL tm
          else 
              let lefts = map (Choice.get << lhand << concl << Choice.get) ths
              let gvs = map (genvar << Choice.get << type_of) lefts
              let pat = Choice.get <| subst (zip gvs lefts) tm
              let abs = list_mk_abs(gvs, pat)
              let th = 
                  rev_itlist (fun y x -> CONV_RULE (THENC (RAND_CONV BETA_CONV) (LAND_CONV BETA_CONV)) (MK_COMB(x, y))) 
                      ths (REFL abs)
              if Choice.get <| rand(concl <| Choice.get th) = tm then REFL tm
              else th
      tm |> Choice.mapError (fun _ -> Exception "SUBS_CONV")
  
  (* ------------------------------------------------------------------------- *)
  (* Get a few rules.                                                          *)
  
negative.code: 
  /// Beta-reduces all the beta-redexes in the conclusion of a theorem.
  let BETA_RULE = CONV_RULE(REDEPTH_CONV BETA_CONV)
  
  /// Reverses the first equation(s) encountered in a top-down search.
  let GSYM = CONV_RULE(ONCE_DEPTH_CONV SYM_CONV)
  
  /// Makes simple term substitutions in a theorem using a given list of theorems.
  let SUBS ths = CONV_RULE(SUBS_CONV ths)
  
  