diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 418c43e9f..b7d048a1e 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -37,13 +37,15 @@ public class AST extends Z3Object
      **/
     public boolean equals(Object o)
     {
-	AST casted = null;
+        AST casted = null;
 
-	try {
-	    casted = AST.class.cast(o);
-	} catch (ClassCastException e) {
-	    return false;
-	}
+        try
+        {
+            casted = AST.class.cast(o);
+        } catch (ClassCastException e)
+        {
+            return false;
+        }
 
         return this.NativeObject() == casted.NativeObject();
     }
@@ -60,18 +62,20 @@ public class AST extends Z3Object
             return 1;
 
         AST oAST = null;
-	try {
-	    AST.class.cast(other);
-	} catch (ClassCastException e) {
-	    return 1;
-	}
+        try
+        {
+            oAST = AST.class.cast(other);
+        } catch (ClassCastException e)
+        {
+            return 1;
+        }
 
-	if (Id() < oAST.Id())
-	    return -1;
-	else if (Id() > oAST.Id())
-	    return +1;
-	else
-	    return 0;
+        if (Id() < oAST.Id())
+            return -1;
+        else if (Id() > oAST.Id())
+            return +1;
+        else
+            return 0;
     }
 
     /**
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index ba1193b20..8a7449a88 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -497,7 +497,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) {
             throw cmd_exception("invalid using-params combinator, keyword expected", c->get_line(), c->get_pos());
         if (i == num_children)
             throw cmd_exception("invalid using-params combinator, parameter value expected", c->get_line(), c->get_pos());
-        symbol param_name = c->get_symbol();
+        symbol param_name = symbol(smt2_keyword_to_param(c->get_symbol()).c_str());
         c = n->get_child(i);
         i++;
         switch (descrs.get_kind(param_name)) {