anchor.diff:      /// Interprets all of the views in a term over the given definer.
       let interpretTerm
         (definer : FuncDefiner<SVBoolExpr>)
  -      (approx : bool)
  +      (shouldApprox : bool)
         (term : FinalTerm)
         : Result<SymProofTerm, Error> =
  -        let symboolResult =
  +        let interpretedR =
               tryMapTerm
                   (fun { CommandSemantics.Semantics = c } -> ok c)
                   (interpretGView definer)
                   (interpretVFunc definer)
                   term
   
  -        // TODO(CaptainHayashi): don't do this unless the user requested it?
  -        let approxResult =
  -            if approx
  -            then lift Some (bind approxTerm symboolResult)
  +        let approxR =
  +            if shouldApprox
  +            then lift Some (bind approxTerm interpretedR)
               else ok None
   
           lift2
  -            (fun s a ->
  -                { Original = term; SymBool = s; Approx = a })
  -            symboolResult
  -            approxResult
  +            (fun interpreted approx ->
  +                { Original = term; SymBool = interpreted; Approx = approx })
  +            interpretedR
  +            approxR
   
   
       /// <summary>
  
positive.code:         let def, indef = partitionDefiner definer
  
          // Then, convert the indefs to symbols.
          let symconv =
              Mapper.make (Reg >> AVar) (Reg >> BVar)
  
          let idsym : FuncDefiner<SVBoolExpr> =
              indef
  
negative.code:     ///         This consumes the view definitions.
      ///     </para>
      /// </summary>
      /// <param name="shouldApprox">Whether to build approximates.</param>
      /// <param name="model">The model to instantiate.</param>
      /// <returns>
      ///     The model with all views instantiated.
      /// </returns>
      let run
        (shouldApprox : bool)
        (model : Model<CmdTerm<SMBoolExpr, GView<Sym<MarkedVar>>, SMVFunc>,
                       FuncDefiner<SVBoolExpr option>>)
        : Result<Model<SymProofTerm, FuncDefiner<SVBoolExpr option>>, Error> =
        let vs = symboliseIndefinites model.ViewDefs
        tryMapAxioms (interpretTerm vs shouldApprox) model
  