1 files changed, 5 insertions, 7 deletions
diff --git a/src/expr/expr.h b/src/expr/expr.h
index 0fcb5ea6a..a16ffee13 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -24,12 +24,10 @@ namespace CVC4 {
   class Expr;
 }/* CVC4 namespace */
 
-namespace std {
-inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC;
-}
-
 namespace CVC4 {
 
+inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC;
+
 class ExprManager;
 
 namespace expr {
@@ -116,13 +114,13 @@ public:
 
 #include "expr/expr_value.h"
 
-inline std::ostream& std::operator<<(std::ostream& out, CVC4::Expr e) {
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream& out, CVC4::Expr e) {
   e.toString(out);
   return out;
 }
 
-namespace CVC4 {
-
 inline Kind Expr::getKind() const {
   return Kind(d_ev->d_kind);
 }