anchor.diff:          let ass_list = zip pats (zip preds (zip thl beta_fns))
           let mnet = itlist (fun p n -> Choice.get <| enter [] (p, p) n) pats empty_net
           let look_fn t =
  -            mapfilter (fun p -> 
  -                    if (Choice.isResult << term_match [] p) t
  -                    then Some p
  -                    else None) (Choice.get <| lookup t mnet)
  +            // CLEAN : Rename this value to something reasonable.
  +            let foo1 = Choice.get <| lookup t mnet
  +            foo1
  +            |> mapfilter (fun p ->
  +                if Choice.isResult <| term_match [] p t then
  +                    Some p
  +                else None) 
  +
           fun top tm -> 
               let pred t = not(look_fn t = []) && free_in t tm
               let stm = 
  -                if top
  -                then Choice.get <| find_term pred tm
  -                else hd(sort free_in (Choice.get <| find_terms pred tm))
  +                if top then
  +                    Choice.get <| find_term pred tm
  +                else
  +                    hd(sort free_in (Choice.get <| find_terms pred tm))
               let pat = hd(look_fn stm)
               let _, tmin, tyin = Choice.get <| term_match [] pat stm
               let pred, (th, beta_fn) =
  
positive.code: /// Apply a higher-order instantiation to a term.
  let instantiate : instantiation -> term -> Choice<term, exn> = 
      let betas n tm = 
          let args, lam = funpow n (fun (l, t) -> (Choice.get <| rand t) :: l, Choice.get <| rator t) ([], tm)
          rev_itlist (fun a l -> 
                  let v, b = Choice.get <| dest_abs l
                  Choice.get <| vsubst [a, v] b) args lam
      let rec ho_betas bcs pat tm = 
          if is_var pat || is_const pat then
              fail()
          else 
              try 
                  let bv, bod = Choice.get <| dest_abs tm
                  Choice.get <| mk_abs(bv, ho_betas bcs (Choice.get <| body pat) bod)
              with
              | Failure _ -> 
                  let hop, args = strip_comb pat
                  try 
                      let n =
                          rev_assoc hop bcs
                          |> Option.getOrFailWith "find"
                      if length args = n
                      then betas n tm
                      else fail()
                  with
                  | Failure _ -> 
                      let lpat, rpat = Choice.get <| dest_comb pat
                      let ltm, rtm = Choice.get <| dest_comb tm
                      try 
  
negative.code:                     if compare tm' tm = 0 then 
                          return! fth
                      else 
                          return!
                              SUBS [ALPHA tm' tm] fth
                              |> Choice.mapError (fun e -> nestedFailure e "PART_MATCH: Sanity check failure")
              }
      PART_MATCH, GEN_PART_MATCH
  
  