anchor.diff:  
   /// Produce distinctness theorem for an inductive type.
   let distinctness ty =
  -    assoc ty (!distinctness_store)
  -    |> Option.getOrFailWith "find"
  +    match assoc ty (!distinctness_store) with
  +    | Some x -> x
  +    | None -> Choice.failwith "find"
   
   /// Produce injectivity theorem for an inductive type.
   let injectivity ty =
  -    assoc ty (!injectivity_store)
  -    |> Option.getOrFailWith "find"
  +    match assoc ty (!injectivity_store) with
  +    | Some x -> x
  +    | None -> Choice.failwith "find"
   
   /// Produce cases theorem for an inductive type.
   let cases ty = 
  -    if ty = "num"
  -    then num_CASES
  -    else 
  -        let _, ith, _ =
  -            assoc ty (!inductive_type_store)
  -            |> Option.getOrFailWith "find"
  -        prove_cases_thm ith
  +    choice {
  +        if ty = "num" then 
  +            return! num_CASES
  +        else 
  +            let! _, ith, _ =
  +                assoc ty (!inductive_type_store)
  +                |> Option.toChoiceWithError "find"
  +
  +            return! prove_cases_thm ith
  +    }
   
   (* ------------------------------------------------------------------------- *)
   (* Convenient definitions for type isomorphism.                              *)
  
positive.code: 
  /// Extends internal store of distinctness and injectivity theorems for a new inductive type.
  let extend_rectype_net(tyname, (_, _, rth)) = 
      let ths1 = 
          try 
              [prove_constructors_distinct rth]
          with
          | Failure _ -> []
      let ths2 = 
          try 
              [prove_constructors_injective rth]
          with
          | Failure _ -> []
      let canon_thl = itlist (fun x y -> Choice.get <| mk_rewrites false x y) (ths1 @ ths2) []
      distinctness_store := map (fun th -> tyname, th) ths1 @ (!distinctness_store)
      injectivity_store := map (fun th -> tyname, th) ths2 @ (!injectivity_store)
      basic_rectype_net := itlist (fun x y -> Choice.get <| net_of_thm true x y) canon_thl (!basic_rectype_net)
  
  do_list extend_rectype_net (!inductive_type_store);;
  
  (* ------------------------------------------------------------------------- *)
  (* Return distinctness and injectivity for a type by simple lookup.          *)
  
negative.code: /// Proves a structural cases theorem for an automatically-defined concrete type.
  let prove_cases_thm = 
      let mk_exclauses x rpats = 
          choice {
              let! xts = Choice.List.map (fun t -> 
                              choice {
                                  let! tm = mk_eq(x, t)
                                  return list_mk_exists(frees t, tm)
                              }) rpats
              return! mk_abs(x, list_mk_disj xts)
          }
  
      let prove_triv tm = 
          choice {
              let evs, bod = strip_exists tm
              let! l, r = dest_eq bod
              if l = r then 
                  return! REFL l
              else 
                  let lf, largs = strip_comb l
                  let rf, rargs = strip_comb r
                  if lf = rf then 
                      let! ths = Choice.List.map (Choice.map ASSUME << mk_eq) (zip rargs largs)
                      let th1 = rev_itlist (C(curry MK_COMB)) ths (REFL lf)
                      let! tms = Choice.List.map (Choice.map concl) ths
                      return! itlist EXISTS_EQUATION tms (SYM th1)
                  else 
                      return! Choice.failwith "prove_triv"
          }
  
      let rec prove_disj tm = 
          choice {
              if is_disj tm then 
                  let! l, r = dest_disj tm
                  return! 
                      DISJ1 (prove_triv l) r
                      |> Choice.bindError (fun _ -> DISJ2 l (prove_disj r))
              else 
                  return! prove_triv tm
          }
  
      let prove_eclause tm = 
          choice {
              let avs, bod = strip_forall tm
              let! ctm = 
                  choice {
                      if is_imp bod then 
                          return! rand bod
                      else 
                          return bod
                  }
  
              let cth = prove_disj ctm
              let dth = 
                  choice {
                      if is_imp bod then 
                          let! tm = lhand bod
                          return! DISCH tm cth
                      else 
                          return! cth
                  }
  
              return! GENL avs dth
          }
  
      fun th -> 
          choice {
              let! th = th
  
              let avs, bod = strip_forall(concl th)
              let! tm1 = lhand bod
              let cls = map (snd << strip_forall) (conjuncts tm1)
              let! pats = 
                  Choice.List.map (fun t -> 
                      choice {
                          if is_imp t then
                              return! rand t
                          else 
                              return t
                      }) cls
  
              let! spats = Choice.List.map dest_comb pats
              let preds = itlist (insert << fst) spats []
              let rpatlist = map (fun pr -> map snd (filter (fun (p, x) -> p = pr) spats)) preds
              let! tys = Choice.List.map (type_of << hd) rpatlist
              let! xs = make_args "x" (freesl pats) tys
              let! xpreds = Choice.List.map2 mk_exclauses xs rpatlist
              let! ith = BETA_RULE(INST (zip xpreds preds) (SPEC_ALL (Choice.result th)))
              let! (tm1, _) = dest_imp(concl ith)
              let eclauses = conjuncts(tm1)
              return! MP (Choice.result ith) (end_itlist CONJ (map prove_eclause eclauses))
          };;
  
  inductive_type_store 
  := ["list", (2, list_INDUCT, list_RECURSION)
  