anchor.diff:          let PRERULE = GEN_REWRITE_RULE (funpow 3 RAND_CONV) (map SYM conthms)
           let IPRULE = SYM << GEN_REWRITE_RULE I (map snd tybijpairs)
           fun rthm tm -> 
  -            let avs, bimp = strip_forall tm
  -            if is_imp bimp
  -            then 
  -                let ant, con = Choice.get <| dest_imp bimp
  -                let ths = map (CONV_RULE BETA_CONV) (CONJUNCTS(ASSUME ant))
  -                let tths, pths = unzip(map CONJ_PAIR ths)
  -                let tth = MATCH_MP (SPEC_ALL rthm) (end_itlist CONJ tths)
  -                let mths = map IPRULE (tth :: tths)
  -                let conth1 = BETA_CONV con
  -                let contm1 = Choice.get <| rand(concl <| Choice.get conth1)
  -                let conth2 = 
  -                    TRANS conth1 
  -                        (AP_TERM (Choice.get <| rator contm1) 
  -                             (SUBS_CONV (tl mths) (Choice.get <| rand contm1)))
  -                let conth3 = PRERULE conth2
  -                let lctms = map (concl << Choice.get) pths
  -                let asmin = Choice.get <| mk_imp(list_mk_conj lctms, Choice.get <| rand(Choice.get <| rand(concl <| Choice.get conth3)))
  -                let argsin = map (Choice.get << rand) (conjuncts(Choice.get <| lhand asmin))
  -                let argsgen = 
  -                    map (fun tm -> mk_var(fst(Choice.get <| dest_var(Choice.get <| rand tm)), Choice.get <| type_of tm)) 
  -                        argsin
  -                let asmgen = Choice.get <| subst (zip argsgen argsin) asmin
  -                let asmquant = 
  -                    list_mk_forall(snd(strip_comb(Choice.get <| rand(Choice.get <| rand asmgen))), asmgen)
  -                let th1 = INST (zip argsin argsgen) (SPEC_ALL(ASSUME asmquant))
  -                let th2 = MP th1 (end_itlist CONJ pths)
  -                let th3 = EQ_MP (SYM conth3) (CONJ tth th2)
  -                DISCH asmquant (GENL avs (DISCH ant th3))
  -            else 
  -                let con = bimp
  -                let conth2 = BETA_CONV con
  -                let tth = PART_MATCH Choice.result rthm (Choice.get <| lhand(Choice.get <| rand(concl <| Choice.get conth2)))
  -                let conth3 = PRERULE conth2
  -                let asmgen = Choice.get <| rand(Choice.get <| rand(concl <| Choice.get conth3))
  -                let asmquant = 
  -                    list_mk_forall(snd(strip_comb(Choice.get <| rand asmgen)), asmgen)
  -                let th2 = SPEC_ALL(ASSUME asmquant)
  -                let th3 = EQ_MP (SYM conth3) (CONJ tth th2)
  -                DISCH asmquant (GENL avs th3)
  +            choice {
  +                let avs, bimp = strip_forall tm
  +                if is_imp bimp then 
  +                    let! ant, con = dest_imp bimp
  +                    let ths = map (CONV_RULE BETA_CONV) (CONJUNCTS(ASSUME ant))
  +                    let tths, pths = unzip(map CONJ_PAIR ths)
  +                    let tth = MATCH_MP (SPEC_ALL rthm) (end_itlist CONJ tths)
  +                    let mths = map IPRULE (tth :: tths)
  +                    let! conth1 = BETA_CONV con
  +                    let! contm1 = rand(concl conth1)
  +                    let! tm1 = rator contm1
  +                    let! tm2 = rand contm1
  +                    let conth2 = TRANS (Choice.result conth1) (AP_TERM tm1 (SUBS_CONV (tl mths) tm2))
  +
  +                    let conth3 = PRERULE conth2
  +                    let! lctms = Choice.List.map (Choice.map concl) pths
  +                    let! tm3 = (Choice.bind rand << Choice.bind rand << Choice.map concl) conth3
  +                    let! asmin = mk_imp(list_mk_conj lctms, tm3)
  +                    let! tm4 = lhand asmin
  +                    let! argsin = Choice.List.map rand (conjuncts tm4)
  +                    let! argsgen = 
  +                        Choice.List.map (fun tm -> 
  +                            choice {
  +                                let! tm1 = rand tm
  +                                let! (s, _) = dest_var tm1
  +                                let! ty1 = type_of tm
  +                                return mk_var(s, ty1)
  +                            }) argsin
  +
  +                    let! asmgen = subst (zip argsgen argsin) asmin
  +
  +                    let asmquant = list_mk_forall(snd(strip_comb(Choice.get <| rand(Choice.get <| rand asmgen))), asmgen)
  +
  +                    let th1 = INST (zip argsin argsgen) (SPEC_ALL(ASSUME asmquant))
  +                    let th2 = MP th1 (end_itlist CONJ pths)
  +                    let th3 = EQ_MP (SYM conth3) (CONJ tth th2)
  +                    return! DISCH asmquant (GENL avs (DISCH ant th3))
  +                else 
  +                    let con = bimp
  +                    let conth2 = BETA_CONV con
  +                    let tth = PART_MATCH Choice.result rthm (Choice.get <| lhand(Choice.get <| rand(concl <| Choice.get conth2)))
  +                    let conth3 = PRERULE conth2
  +                    let! tm1 = Choice.bind (rand << concl) conth3
  +                    let! asmgen = rand tm1
  +                    let asmquant = list_mk_forall(snd(strip_comb(Choice.get <| rand asmgen)), asmgen)
  +                    let th2 = SPEC_ALL(ASSUME asmquant)
  +                    let th3 = EQ_MP (SYM conth3) (CONJ tth th2)
  +                    return! DISCH asmquant (GENL avs th3)
  +            }
   
       (* ----------------------------------------------------------------------- *)
       (* Finish off a consequence of the induction theorem.                      *)
  
positive.code:             let mkindex = 
                  map (fun t -> hd(tl(snd(Choice.get <| dest_type(Choice.get <| type_of t)))), t) mks
              fun cth -> 
                  let artms = snd(strip_comb(Choice.get <| rand(Choice.get <| rand(concl <| Choice.get cth))))
                  let artys = mapfilter (Choice.toOption << Choice.bind type_of << rand) artms
                  let args, bod = strip_abs(Choice.get <| rand(hd(hyp <| Choice.get cth)))
                  let ccitm, rtm = Choice.get <| dest_comb bod
                  let cctm, itm = Choice.get <| dest_comb ccitm
                  let rargs, iargs = partition (C free_in rtm) args
                  let xths = map (extract_arg itm) iargs
                  let cargs' = map (Choice.get << subst [i, itm] << Choice.get << lhand << concl <<Choice.get) xths
                  let indices = map sucivate (0 -- (length rargs - 1))
                  let rindexed = map (curry (Choice.get << mk_comb) r) indices
                  let rargs' = 
                      map2 (fun a rx -> Choice.get <| mk_comb(Option.getOrFailWith "find" <| assoc a mkindex, rx)) artys 
                          rindexed
                  let sargs' = map (curry (Choice.get << mk_comb) s) indices
                  let allargs = cargs' @ rargs' @ sargs'
                  let funty = itlist ((fun ty -> Choice.get << mk_fun_ty ty) << Choice.get << type_of) allargs zty
                  let funname = 
                      fst(Choice.get <| dest_const(repeat (Choice.toOption << rator) (Choice.get <| lhand(concl <| Choice.get cth)))) + "'"
                  let funarg = mk_var(funname, funty)
                  list_mk_abs([i; r; s], list_mk_comb(funarg, allargs))
  
      (* ----------------------------------------------------------------------- *)
      (* Derive the recursion theorem.                                           *)
  
negative.code:                 Choice.get <| mk_type("sum", [mk_sum tys1; mk_sum tys2])
          let mk_inls = 
              let rec mk_inls ty = 
                  choice {
                      if is_vartype ty then 
                          return [mk_var("x", ty)]
                      else
                          let! ty1 = dest_type ty
                          match ty1 with
                          | _, [ty1; ty2] -> 
                              let! inls1 = mk_inls ty1
                              let! inls2 = mk_inls ty2
                              let! inl = mk_const("INL", [ty1, aty;
                                                          ty2, bty])
                              let! inr = mk_const("INR", [ty1, aty;
                                                          ty2, bty])
                              let! tms1 = Choice.List.map (curry mk_comb inl) inls1
                              let! tms2 = Choice.List.map (curry mk_comb inr) inls2
                              return tms1 @ tms2
                          | _ -> 
                              return! Choice.failwith "mk_inls: Unhandled case."
                  }
  
              fun ty -> 
                  let bods = Choice.get <| mk_inls ty
                  map (fun t -> Choice.get <| mk_abs(Choice.get <| find_term is_var t, t)) bods
  
          let mk_outls = 
              let rec mk_inls sof ty = 
                  if is_vartype ty
  