anchor.diff:          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, _ = itlist SCRUB_EQUATION (hyp <| Choice.get th5) (th5, [])
  +        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(itlist SCRUB_EQUATION (hyp <| Choice.get th7) (th7, []))
  +        fst(Choice.get <| Choice.List.fold (fun acc x -> SCRUB_EQUATION x acc) (th7, []) (hyp <| Choice.get th7))
   
       (* ----------------------------------------------------------------------- *)
       (* Create the recursive functions and eliminate pseudo-constructors.       *)
  
positive.code:         let th1 = ASSUME(Option.get <| find (fun eq -> Choice.get <| lhand eq = epred) (hyp <| Choice.get exth))
          let th2 = TRANS th1 (SUBS_CONV cdefs (Choice.get <| rand(concl <| Choice.get th1)))
          let th3 = EQ_MP (AP_THM th2 (Choice.get <| rand extm)) exth
          let th4, _ = itlist SCRUB_EQUATION (hyp <| Choice.get th3) (th3, [])
          let mkname = "_mk_" + ename
          let destname = "_dest_" + ename
          let bij1, bij2 = new_basic_type_definition ename (mkname, destname) th4
  
negative.code:         let pasms = filter (C mem (map fst consindex) << Choice.get << lhand) (hyp <| Choice.get fxth5)
          let fxth6 = itlist DISCH pasms fxth5
          let fxth7, _ = 
              Choice.get <| Choice.List.fold (fun acc x -> SCRUB_EQUATION x acc) (fxth6, []) (itlist (union << hyp << Choice.get) conthms []) 
          let fxth8 = UNDISCH_ALL fxth7
          fst(Choice.get <| Choice.List.fold (fun acc x -> SCRUB_EQUATION x acc) (fxth8, []) (subtract (hyp <| Choice.get fxth8) eqs) )
  
      (* ----------------------------------------------------------------------- *)
      (* Create a function for recursion clause.                                 *)
  