anchor.diff:  
           /// Tests the viewdef LHS translator.
           [<TestCaseSource("ViewFuncs")>]
  -        member x.``the view func translator works correctly`` (v: OView) =
  -            v |> funcOfView (NUnit.Globals
  -                             |> Map.toSeq
  -                             |> Seq.map (function
  -                                         | (x, Type.Int ()) -> x |> siBefore |> Expr.Int
  -                                         | (x, Type.Bool ()) -> x |> sbBefore |> Expr.Bool))
  +        member x.``the view func translator works correctly`` (v : OView) =
  +            v
  +            |> flattenFuncSeq
  +                   (NUnit.Globals
  +                    |> Map.toSeq
  +                    |> Seq.map
  +                           (function
  +                            | (x, Type.Int ()) -> x |> siBefore |> Expr.Int
  +                            | (x, Type.Bool ()) -> x |> sbBefore |> Expr.Bool))
  
positive.code: open Starling.Core.GuardedView
  
  
  (*
   * View-to-func flattening.
   *)
  
  /// Extracts a sequence of all of the parameters in a view in order.
  let paramsOfView ms =
      ms
      |> Seq.map (fun v -> v.Params)
      |> Seq.concat
  
  /// Constructs a (hopefully) unique name for a func encompassing a view.
  let funcNameOfView : Func<'a> seq ->  string =
      fun ms ->
      ms
      // These two steps are to ensure we don't capture an existing name.
      |> Seq.map (fun { Name = n } -> n.Replace("_", "__"))
      |> scons "v"
      |> String.concat "_"
      |> (fun s -> if s = "v" then "emp" else s)
  
  /// Constructs a Func from a View, given a set of active globals in the
  /// appropriate format for appending into the func's parameter list.
  /// and some transformer from the parameters to expressions.
  let funcOfView globals view =
      { Name = view |> funcNameOfView
        Params = view |> paramsOfView |> Seq.append globals |> List.ofSeq }
  
  (*
   * View usages
   *)
  
  /// Adds the globals in gs to the argument lists of a view assertion.
  let addGlobalsToViewSet gs =
     Seq.map (mapItem (funcOfView gs)) >> Multiset.ofFlatSeq
  
  /// Adds the globals in gs to the argument list of the assertions in a term.
  let addGlobalsToTerm gs _ =
      mapTerm id
              (addGlobalsToViewSet (gs Before))
              (funcOfView (gs After))
  
  (*
   * View definitions
   *)
  
  /// Adds the globals in gs to a defining view.
  let addGlobalsToViewDef gs =
      function
      | Definite (v, d) -> Definite (funcOfView gs v, d)
      | Indefinite v -> Indefinite (funcOfView gs v)
  
  (*
   * Whole models
   *)
  
  /// Adds globals to the arguments of all views in a model.
  let flatten (mdl: UVModel<Term<'cmd, Set<GuardedSubview>, OView>>) =
      /// Build a function making a list of global arguments, for view assertions.
      let gargs marker = varMapToExprs (marker >> Reg) mdl.Globals
  
      /// Build a list of global parameters, for view definitions.
      let gpars =
          mdl.Globals
          |> Map.toSeq
          |> Seq.map (fun (name, ty) -> withType ty name)
          |> List.ofSeq
  
      {Globals = mdl.Globals
       Locals = mdl.Locals
       Axioms = Map.map (addGlobalsToTerm gargs) mdl.Axioms
       ViewDefs = List.map (addGlobalsToViewDef gpars) mdl.ViewDefs
       Semantics = mdl.Semantics}
  
  
  /// <summary>
  
negative.code:         /// Tests the view predicate name generator.
          [<TestCaseSource("ViewFuncNamings")>]
          member x.``the flattened view name generator generates names correctly`` v =
              (genFlatFuncSeqName : OView -> string) v
  
          /// Test cases for the full defining-view func converter.
          /// These all use the Globals environment above.
  