1 files changed, 2 insertions, 2 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 952caf89e..ba062c20f 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -71,13 +71,13 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
   }
 }
 
-void Printer::toStream(std::ostream& out, const Model& m) const
+void Printer::toStream(std::ostream& out, const smt::Model& m) const
 {
   for(size_t i = 0; i < m.getNumCommands(); ++i) {
     const NodeCommand* cmd = m.getCommand(i);
     const DeclareFunctionNodeCommand* dfc =
         dynamic_cast<const DeclareFunctionNodeCommand*>(cmd);
-    if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction().toExpr()))
+    if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction()))
     {
       continue;
     }