anchor.diff:          |> Choice.bindError (fun _ -> REFL tm)
       EQT_ELIM sth
       |> Choice.bindError (fun _ ->
  -        let tth = 
  -            tryfind (fun pr -> Choice.toOption <| apply_prover pr (Choice.get <| rand(concl <| Choice.get sth))) provers
  -            |> Option.toChoiceWithError "tryfind"
  -        EQ_MP (SYM sth) tth)
  +        choice {
  +            let! tm = Choice.bind (rand << concl)  sth
  +            let tth = 
  +                tryfind (fun pr -> Choice.toOption <| apply_prover pr tm) provers
  +                |> Option.toChoiceWithError "tryfind"
  +            return! EQ_MP (SYM sth) tth
  +            })
   
   (* ------------------------------------------------------------------------- *)
   (* Functions for changing or augmenting components of simpsets.              *)
  
positive.code: // TOP_DEPTH_SQCONV: Applies simplification top-down to all subterms, retraversing changed ones.
  // TOP_SWEEP_SQCONV: Applies simplification top-down at all levels, but after descending to subterms, does not return to higher ones.
  let ONCE_DEPTH_SQCONV, DEPTH_SQCONV, REDEPTH_SQCONV, TOP_DEPTH_SQCONV, TOP_SWEEP_SQCONV = 
      let IMP_REWRITES_CONV strat (Simpset(net, prover, provers, rewmaker) as ss) 
          lev pconvs tm = 
          tryfind (fun (n, cnv) -> 
                  if n >= 4
                  then None
                  else 
                      let th = cnv tm
                      let etm = concl <| Choice.get th
                      if is_eq etm
                      then Choice.toOption th
                      elif lev <= 0
                      then None
                      else 
                          let cth = prover strat ss (lev - 1) (Choice.get <| lhand etm)
                          Choice.toOption <| MP th cth) pconvs
          |> Option.toChoiceWithError "IMP_REWRITES_CONV: Too deep"
  
      let rec RUN_SUB_CONV strat ss lev triv th = 
          let tm = concl <| Choice.get th
          if is_imp tm
          then 
              let subtm = Choice.get <| lhand tm
              let avs, bod = strip_forall subtm
              let (t, t'), ss', mk_fun = 
                  try 
                      Choice.get <| dest_eq bod, ss, I
                  with
                  | Failure _ -> 
                      let cxt, deq = Choice.get <| dest_imp bod
                      Choice.get <| dest_eq deq, AUGMENT_SIMPSET (ASSUME cxt) ss, DISCH cxt
              let eth, triv' = 
                  try 
                      strat ss' lev t, false
                  with
                  | Failure _ -> REFL t, triv
              let eth' = GENL avs (mk_fun eth)
              let th' = 
                  if is_var t'
                  then INST [Choice.get <| rand(concl <| Choice.get eth), t'] th
                  else GEN_PART_MATCH lhand th (concl <| Choice.get eth')
              let th'' = MP th' eth'
              RUN_SUB_CONV strat ss lev triv' th''
          elif triv
          then fail()
          else th
      let GEN_SUB_CONV strat ss lev pconvs tm = 
          let v = 
              tryfind (fun (n, cnv) -> 
                      if n < 4
                      then None
                      else 
                          let th = cnv tm
                          Choice.toOption <| RUN_SUB_CONV strat ss lev true th) pconvs
              |> Option.toChoiceWithError "tryfind"
          v |> Choice.bindError (fun _ ->
                  if is_comb tm
                  then 
                      let l, r = Choice.get <| dest_comb tm
                      let v = 
                          let th1 = strat ss lev l
                          let v = 
                              let th2 = strat ss lev r
                              MK_COMB(th1, th2)
                          v |> Choice.bindError (fun _ -> AP_THM th1 r)
                      v |> Choice.bindError (fun _ -> AP_TERM l (strat ss lev r))
                  elif is_abs tm
                  then 
                      let v, bod = Choice.get <| dest_abs tm
                      let th = strat ss lev bod
                      let v' = 
                          ABS v th
                      v' |> Choice.bindError (fun _ ->
                              let gv = genvar(Choice.get <| type_of v)
                              let gbod = Choice.get <| vsubst [gv, v] bod
                              let gth = ABS gv (strat ss lev 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)
                  else Choice.failwith "GEN_SUB_CONV")
  
      let rec ONCE_DEPTH_SQCONV (Simpset(net, prover, provers, rewmaker) as ss) 
              lev tm : thm = 
          let pconvs = Choice.get <| lookup tm net
          try 
              IMP_REWRITES_CONV ONCE_DEPTH_SQCONV ss lev pconvs tm
          with
          | Failure _ -> GEN_SUB_CONV ONCE_DEPTH_SQCONV ss lev pconvs tm
      let rec DEPTH_SQCONV (Simpset(net, prover, provers, rewmaker) as ss) lev tm = 
          let pconvs = Choice.get <| lookup tm net
          try 
              let th1 = GEN_SUB_CONV DEPTH_SQCONV ss lev pconvs tm
              let tm1 = Choice.get <| rand(concl <| Choice.get th1)
              let pconvs1 = Choice.get <| lookup tm1 net
              try 
                  TRANS th1 (IMP_REWRITES_CONV DEPTH_SQCONV ss lev pconvs1 tm1)
              with
              | Failure _ -> th1
          with
          | Failure _ -> IMP_REWRITES_CONV DEPTH_SQCONV ss lev pconvs tm
      let rec REDEPTH_SQCONV (Simpset(net, prover, provers, rewmaker) as ss) lev 
              tm = 
          let pconvs = Choice.get <| lookup tm net
          let th = 
              try 
                  let th1 = GEN_SUB_CONV REDEPTH_SQCONV ss lev pconvs tm
                  let tm1 = Choice.get <| rand(concl <| Choice.get th1)
                  let pconvs1 = Choice.get <| lookup tm1 net
                  try 
                      TRANS th1 
                          (IMP_REWRITES_CONV REDEPTH_SQCONV ss lev pconvs1 tm1)
                  with
                  | Failure _ -> th1
              with
              | Failure _ -> IMP_REWRITES_CONV REDEPTH_SQCONV ss lev pconvs tm
          try 
              let th' = REDEPTH_SQCONV ss lev (Choice.get <| rand(concl <| Choice.get th))
              TRANS th th'
          with
          | Failure _ -> th
      let rec TOP_DEPTH_SQCONV (Simpset(net, prover, provers, rewmaker) as ss) lev 
              tm = 
          let pconvs = Choice.get <| lookup tm net
          let th1 = 
              try 
                  IMP_REWRITES_CONV TOP_DEPTH_SQCONV ss lev pconvs tm
              with
              | Failure _ -> GEN_SUB_CONV TOP_DEPTH_SQCONV ss lev pconvs tm
          try 
              let th2 = TOP_DEPTH_SQCONV ss lev (Choice.get <| rand(concl <| Choice.get th1))
              TRANS th1 th2
          with
          | Failure _ -> th1
      let rec TOP_SWEEP_SQCONV (Simpset(net, prover, provers, rewmaker) as ss) lev 
              tm = 
          let pconvs = Choice.get <| lookup tm net
          try 
              let th1 = IMP_REWRITES_CONV TOP_SWEEP_SQCONV ss lev pconvs tm
              try 
                  let th2 = TOP_SWEEP_SQCONV ss lev (Choice.get <| rand(concl <| Choice.get th1))
                  TRANS th1 th2
              with
              | Failure _ -> th1
          with
          | Failure _ -> GEN_SUB_CONV TOP_SWEEP_SQCONV ss lev pconvs tm
      ONCE_DEPTH_SQCONV, DEPTH_SQCONV, REDEPTH_SQCONV, TOP_DEPTH_SQCONV, 
      TOP_SWEEP_SQCONV
  
  (* ------------------------------------------------------------------------- *)
  (* Maintenence of basic rewrites and conv nets for rewriting.                *)
  
negative.code: /// Change the method of prover application in a simpset.
  let ss_of_prover newprover (Simpset(net, _, provers, rewmaker)) = 
      Simpset(net, newprover, provers, rewmaker)
  
  /// Add new provers to a simpset.
  let ss_of_provers newprovers (Simpset(net, prover, provers, rewmaker)) = 
      Simpset(net, prover, newprovers @ provers, rewmaker)
  