anchor.diff:      let symboliseIndefinites
         (definer : FuncDefiner<SVBoolExpr option>)
         : Result<FuncDefiner<SVBoolExpr>, Error> =
  +        // First, work out which definitions are indefinite.
           let def, indef = partitionDefiner definer
   
  -        // Then, convert the indefs to symbols.
  -        let symconv =
  +        (* We now need to convert the definitions in 'indefSeq' such that they
  +           map the funcs to a symbol.  We do this by first making some helper
  +           functions. *)
  +
  +        // Lifts variables in an expression into the Sym<> type with Reg.
  +        let exprToSym expr =
               mapTraversal
                   (tliftToExprDest
                       (tliftOverCTyped (ignoreContext (Reg >> ok))))
  -
  +                expr
  +
  +        (* Constructs a definite view definition, given an indefinite view
  +           definition as a pair. *)
  +        let indefiniteFuncToSym ({ Name = n ; Params = ps }, _) =
  +            let convParamsR = collect (List.map exprToSym ps)
  +
  +            let defR =
  +                lift (func (sprintf "!UNDEF:%A" n) >> Sym >> BVar)
  +                    convParamsR
  +
  +            lift (mkPair (func n ps)) defR
  +
  +        // Now apply the above to all indefinites to create a new definer.
           let indefSeq = FuncDefiner.toSeq indef
  -
  -        let symbolise ({ Name = n ; Params = ps }, _) =
  -            let convParamsResult = collect (List.map symconv ps)
  -
  -            let defResult =
  -                lift (func (sprintf "!UNDEF:%A" n) >> Sym >> BVar)
  -                    convParamsResult
  -
  -            lift (mkPair (func n ps)) defResult
  -
  -        let symbolisedResult = collect (Seq.map symbolise indefSeq)
  -        let idsymResult = lift FuncDefiner.ofSeq symbolisedResult
  -
  -        // TODO(CaptainHayashi): use functables properly.
  -        lift (fun idsym -> def @ idsym) (mapMessages Traversal idsymResult)
  +        let indefSymSeqR = collect (Seq.map indefiniteFuncToSym indefSeq)
  +        let indefSymR = lift FuncDefiner.ofSeq indefSymSeqR
  +
  +        // Merge the new definitions into our original definer.
  +        lift (FuncDefiner.combine def) (mapMessages Traversal indefSymR)
   
   
       /// <summary>
  
positive.code:     let approxTerm (symterm : Term<SMBoolExpr, SMBoolExpr, SMBoolExpr>)
        : Result<Term<MBoolExpr, MBoolExpr, MBoolExpr>, Error> =
          (* This is needed to adapt approx's TraversalError<unit> into TraversalError<Error>.
             It's horrible and I hate it. *)
          let toError =
              mapMessages
                  (function
  
negative.code: 
  
      /// <summary>
      ///     Makes all indefinite viewdefs in a definer definite by defining them
      ///     as symbols.
      /// </summary>
      /// <param name="definer">
      ///     The view definer to convert.
  