anchor.diff:       * entry (erroneous or otherwise) in the semantics for this prim.
        * Since this is an error in this case, make it one.
        *)
  -    let actions =
  -        prim
  -        |> wrapMessages Instantiate
  -               (instantiatePrim primSubFun semantics)
  -        |> bind (failIfNone (MissingDef prim))
  -
  -    let f = frame svars tvars >> List.ofSeq >> mkAnd
  -    let aframe = lift (frame svars tvars >> List.ofSeq >> mkAnd) actions
  -    lift2 mkAnd2 actions aframe
  +    prim
  +    |> wrapMessages Instantiate
  +           (instantiatePrim primSubFun semantics)
  +    |> bind (failIfNone (MissingDef prim))
   
   /// Translate a command to an expression characterising it.
   /// This is the sequential composition of the translations of each
  
positive.code:   (svars : VarMap)
    (tvars : VarMap)
    : Command -> Result<SMBoolExpr, Error> =
      Seq.map (semanticsOfPrim semantics svars tvars)
      >> collect
      >> lift (function
               | [] -> frame svars tvars BTrue |> List.ofSeq |> mkAnd
               | xs -> List.reduce composeBools xs)
  
  open Starling.Core.Axiom.Types
  /// Translate a model over Prims to a model over semantic expressions.
  
negative.code:     |> Seq.filter (fun (name, _) -> not (Set.contains name evars))
      |> Seq.map (fun (name, ty) -> frameVar (withType ty name))
  
  /// Translate a primitive command to an expression characterising it
  /// by instantiating the semantics from the core semantics map with
  /// the variables from the command
  let instantiateSemanticsOfPrim
    (semantics : PrimSemanticsMap)
    (svars : VarMap)
    (tvars : VarMap)
  