anchor.diff:              << GEN_REWRITE_RULE LAND_CONV tybij2
           let FINRULE = GEN_REWRITE_RULE RAND_CONV tybij1
           fun th -> 
  -            let av, bimp = Choice.get <| dest_forall(concl <| Choice.get th)
  -            let pv = Choice.get <| lhand(Choice.get <| body(Choice.get <| rator(Choice.get <| rand bimp)))
  -            let p, v = Choice.get <| dest_comb pv
  -            let mk, dest = assoc p consindex |> Option.getOrFailWith "find"
  -            let ty = hd(snd(Choice.get <| dest_type(Choice.get <| type_of dest)))
  -            let v' = mk_var(fst(Choice.get <| dest_var v), ty)
  -            let dv = Choice.get <| mk_comb(dest, v')
  -            let th1 = PRERULE(SPEC dv th)
  -            let th2 = MP th1 (REFL(Choice.get <| rand(Choice.get <| lhand(concl <| Choice.get th1))))
  -            let th3 = CONV_RULE BETA_CONV th2
  -            GEN v' (FINRULE(CONJUNCT2 th3))
  +            choice {
  +                let! th = th
  +                let! av, bimp = dest_forall(concl th)
  +                let! tm1 = rand bimp
  +                let! tm2 = rator tm1
  +                let! tm3 = body tm2
  +                let! pv = lhand tm3
  +                let! p, v = dest_comb pv
  +                let! mk, dest = 
  +                    assoc p consindex 
  +                    |> Option.toChoiceWithError "find"
  +                let! ty1 = type_of dest
  +                let! (_, tys2) = dest_type ty1
  +                let ty = hd tys2
  +                let! (s, _) = dest_var v
  +                let v' = mk_var(s, ty)
  +                let! dv = mk_comb(dest, v')
  +                let! th1 = PRERULE(SPEC dv (Choice.result th))
  +                let! tm4 = lhand(concl th1)
  +                let! tm5 = rand tm4
  +                let th2 = MP (Choice.result th1) (REFL tm5)
  +                let th3 = CONV_RULE BETA_CONV th2
  +                return! GEN v' (FINRULE(CONJUNCT2 th3))
  +            }
   
       (* ----------------------------------------------------------------------- *)
       (* Derive the induction theorem.                                           *)
       (* ----------------------------------------------------------------------- *)
   
       let derive_induction_theorem consindex tybijpairs conthms iith rth = 
  -        let bths = 
  -            map2 (pullback_induction_clause tybijpairs conthms) (CONJUNCTS rth) 
  -                (conjuncts(Choice.get <| lhand(concl <| Choice.get iith)))
  -        let asm = list_mk_conj(map (Choice.get << lhand << concl <<Choice.get) bths)
  -        let ths = map2 MP bths (CONJUNCTS(ASSUME asm))
  -        let th1 = MP iith (end_itlist CONJ ths)
  -        let th2 = 
  -            end_itlist CONJ 
  -                (map (finish_induction_conclusion consindex tybijpairs) 
  -                     (CONJUNCTS th1))
  -        let th3 = DISCH asm th2
  -        let preds = map (Choice.get << rator << Choice.get << body << Choice.get << rand) (conjuncts(Choice.get <| rand(concl <| Choice.get th3)))
  -        let th4 = GENL preds th3
  -        let pasms = filter (C mem (map fst consindex) << Choice.get << lhand) (hyp <| Choice.get th4)
  -        let th5 = itlist DISCH pasms th4
  -        let th6, _ = Choice.get <| Choice.List.fold (fun acc x -> SCRUB_EQUATION x acc) (th5, []) (hyp <| Choice.get th5)
  -        let th7 = UNDISCH_ALL th6
  -        fst(Choice.get <| Choice.List.fold (fun acc x -> SCRUB_EQUATION x acc) (th7, []) (hyp <| Choice.get th7))
  +        choice {
  +            let! iith = iith
  +            let! tm1 = lhand(concl iith)
  +            let bths = map2 (pullback_induction_clause tybijpairs conthms) (CONJUNCTS rth) (conjuncts tm1)
  +            let! tms = Choice.List.map (Choice.bind lhand << Choice.map concl) bths
  +            let asm = list_mk_conj tms
  +            let ths = map2 MP bths (CONJUNCTS(ASSUME asm))
  +            let th1 = MP (Choice.result iith) (end_itlist CONJ ths)
  +            let th2 = end_itlist CONJ (map (finish_induction_conclusion consindex tybijpairs) (CONJUNCTS th1))
  +            let! th3 = DISCH asm th2
  +
  +            let! tm2 = rand(concl th3)
  +            let! preds = Choice.List.map (Choice.bind rator << Choice.bind body << rand) (conjuncts tm2)
  +
  +            let th4 = GENL preds (Choice.result th3)
  +            let! tms1 = Choice.map hyp th4
  +            let! pasms = Choice.List.filter (Choice.map (C mem (map fst consindex)) << lhand) tms1
  +
  +            let th5 = itlist DISCH pasms th4
  +            let! tms2 = Choice.map hyp th5
  +            let! th6, _ = Choice.List.fold (fun acc x -> SCRUB_EQUATION x acc) (th5, []) tms2
  +            let th7 = UNDISCH_ALL th6
  +            let! tms3 = Choice.map hyp th7
  +            let! (th8, _) = Choice.List.fold (fun acc x -> SCRUB_EQUATION x acc) (th7, []) tms3
  +            return! th8
  +        }
   
       (* ----------------------------------------------------------------------- *)
       (* Create the recursive functions and eliminate pseudo-constructors.       *)
  
positive.code:                 Choice.get <| mk_type("sum", [mk_sum tys1; mk_sum tys2])
          let mk_inls = 
              let rec mk_inls ty = 
                  if is_vartype ty
                  then [mk_var("x", ty)]
                  else 
                      match Choice.get <| dest_type ty with
                      | _, [ty1; ty2] -> 
                          let inls1 = mk_inls ty1
                          let inls2 = mk_inls ty2
                          let inl = 
                              Choice.get <| mk_const("INL", [ty1, aty; ty2, bty])
                          let inr = 
                              Choice.get <| mk_const("INR", [ty1, aty; ty2, bty])
                          map (curry (Choice.get << mk_comb) inl) inls1 
                          @ map (curry (Choice.get << mk_comb) inr) inls2
                      | _ -> failwith "mk_inls: Unhnadled case."
              fun ty -> 
                  let bods = 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
  
negative.code:                     | _ -> failwith "mk_outls: Unhandled case."
              fun ty -> 
                  let x = mk_var("x", ty)
                  Choice.get <| Choice.List.map (curry mk_abs x) (mk_inls x ty)
          let mk_newfun fn outl = 
              let s, ty = Choice.get <| dest_var fn
              let dty = hd(snd(Choice.get <| dest_type ty))
  