Minor refactorings, in response to code review (Bug #73)

3 files changed, 8 insertions, 8 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6a2640080..bb665ef81 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -184,9 +184,9 @@ Type* ExprManager::mkSort(const std::string& name) {
   return d_nodeManager->mkSort(name);
 }
 
-Expr ExprManager::mkVar(Type* type, const std::string& name) {
+Expr ExprManager::mkVar(const std::string& name, Type* type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
+  return Expr(this, new Node(d_nodeManager->mkVar(name, type)));
 }
 
 Expr ExprManager::mkVar(Type* type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 1c1d6dbd7..82698732c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -192,7 +192,7 @@ public:
   Type* mkSort(const std::string& name);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(Type* type, const std::string& name);
+  Expr mkVar(const std::string& name, Type* type);
   Expr mkVar(Type* type);
 
   /** Returns the minimum arity of the given kind. */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 83f28a842..2b403ad36 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -270,11 +270,11 @@ public:
   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
   /**
-   * Create a variable with the given type and name.  NOTE that no
-   * lookup is done on the name.  If you mkVar(type, "a") and then
-   * mkVar(type, "a") again, you have two variables.
+   * Create a variable with the given name and type.  NOTE that no
+   * lookup is done on the name.  If you mkVar("a", type) and then
+   * mkVar("a", type) again, you have two variables.
    */
-  Node mkVar(Type* type, const std::string& name);
+  Node mkVar(const std::string& name, Type* type);
 
   /** Create a variable with the given type. */
   Node mkVar(Type* type);
@@ -767,7 +767,7 @@ inline Node NodeManager::mkNode(Kind kind,
   return NodeBuilder<>(this, kind).append(children);
 }
 
-inline Node NodeManager::mkVar(Type* type, const std::string& name) {
+inline Node NodeManager::mkVar(const std::string& name, Type* type) {
   Node n = mkVar(type);
   n.setAttribute(expr::VarNameAttr(), name);
   return n;