2 files changed, 31 insertions, 25 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 213171124..5c3f1b771 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -20,26 +20,6 @@ namespace CVC4 {
 namespace expr {
 
 #ifdef CVC4_DEBUG
-
-/**
- * Pretty printer for use within gdb.  This is not intended to be used
- * outside of gdb.  This writes to the Warning() stream and immediately
- * flushes the stream.
- *
- * Note that this function cannot be a template, since the compiler
- * won't instantiate it.  Even if we explicitly instantiate.  (Odd?)
- * So we implement twice.
- */
-void CVC4_PUBLIC debugPrint(const NodeTemplate<true>& n) {
-  n.printAst(Warning(), 0);
-  Warning().flush();
-}
-
-void CVC4_PUBLIC debugPrint(const NodeTemplate<false>& n) {
-  n.printAst(Warning(), 0);
-  Warning().flush();
-}
-
 #endif /* CVC4_DEBUG */
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index 06f368583..25f0b7453 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -65,8 +65,8 @@ template<bool ref_count>
   class NodeTemplate {
 
     /**
-     * The NodeValue has access to the private constructors, so that the iterators
-     * can can create new nodes.
+     * The NodeValue has access to the private constructors, so that the
+     * iterators can can create new nodes.
      */
     friend class NodeValue;
 
@@ -100,8 +100,8 @@ template<bool ref_count>
 
     /**
      * Assigns the expression value and does reference counting. No assumptions
-     * are made on the expression, and should only be used if we know what we are
-     * doing.
+     * are made on the expression, and should only be used if we know what we 
+     * are doing.
      *
      * @param ev the expression value to assign
      */
@@ -575,7 +575,7 @@ template<bool ref_count>
     if(ref_count)
       d_nv->dec();
     Assert(ref_count || d_nv->d_rc > 0,
-        "Temporary node pointing to an expired node");
+           "Temporary node pointing to an expired node");
   }
 
 template<bool ref_count>
@@ -675,6 +675,32 @@ template<bool ref_count>
     return NodeManager::currentNM()->getType(*this);
   }
 
+
+
+/**
+ * Pretty printer for use within gdb.  This is not intended to be used
+ * outside of gdb.  This writes to the Warning() stream and immediately
+ * flushes the stream.
+ *
+ * Note that this function cannot be a template, since the compiler
+ * won't instantiate it.  Even if we explicitly instantiate.  (Odd?)
+ * So we implement twice.
+ *
+ * Tim's Note: I moved this into the node.h file because this allows gdb
+ * to find the symbol, and use it, which is the first standard this code needs
+ * to meet. A cleaner solution is welcomed.
+ */
+static void CVC4_PUBLIC debugPrintNode(const NodeTemplate<true>& n) {
+  n.printAst(Warning(), 0);
+  Warning().flush();
+}
+
+static void CVC4_PUBLIC debugPrintTNode(const NodeTemplate<false>& n) {
+  n.printAst(Warning(), 0);
+  Warning().flush();
+}
+
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_H */