diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp
index 6cdfe1623..efcab14ea 100644
--- a/src/shell/datalog_frontend.cpp
+++ b/src/shell/datalog_frontend.cpp
@@ -43,17 +43,7 @@ static datalog::context * g_ctx = 0;
 static datalog::rule_set * g_orig_rules;
 static datalog::instruction_block * g_code;
 static datalog::execution_context * g_ectx;
-static smt_params * g_params;
 
-datalog_params::datalog_params():
-    m_default_table("sparse"),
-    m_default_table_checked(false)
-{}
-
-// void datalog_params::register_params(ini_params& p) {
-//    p.register_symbol_param("DEFAULT_TABLE", m_default_table, "Datalog engine: default table (sparse)");
-//    p.register_bool_param("DEFAULT_TABLE_CHECKED", m_default_table_checked, "Wrap default table with a sanity checker");
-// }
 
 static void display_statistics(
     std::ostream& out,
@@ -61,7 +51,6 @@ static void display_statistics(
     datalog::rule_set& orig_rules,
     datalog::instruction_block& code,
     datalog::execution_context& ex_ctx,
-    smt_params& params,
     bool verbose
     ) 
 {
@@ -109,7 +98,7 @@ static void display_statistics(
 
 static void display_statistics() {
     if (g_ctx) {
-        display_statistics(std::cout, *g_ctx, *g_orig_rules, *g_code, *g_ectx, *g_params, true);
+        display_statistics(std::cout, *g_ctx, *g_orig_rules, *g_code, *g_ectx, true);
     }
 }
 
@@ -127,7 +116,6 @@ static void on_ctrl_c(int) {
 
 unsigned read_datalog(char const * file) {
     IF_VERBOSE(1, verbose_stream() << "Z3 Datalog Engine\n";);
-    datalog_params dl_params;
     smt_params     s_params;
     ast_manager m;
     g_overall_time.start();
@@ -135,8 +123,6 @@ unsigned read_datalog(char const * file) {
     signal(SIGINT, on_ctrl_c);
     params_ref params;
     params.set_sym("engine", symbol("datalog"));
-    params.set_sym("default_table", dl_params.m_default_table);
-    params.set_bool("default_table_checked", dl_params.m_default_table_checked);
 
     datalog::context ctx(m, s_params, params);
     datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
@@ -186,7 +172,6 @@ unsigned read_datalog(char const * file) {
     g_orig_rules = &original_rules;
     g_code = &rules_code;
     g_ectx = &ex_ctx;
-    g_params = &s_params;
 
     try {    
         g_piece_timer.reset();
@@ -254,7 +239,6 @@ unsigned read_datalog(char const * file) {
             original_rules, 
             rules_code,
             ex_ctx,
-            s_params,
             false);
 
     }
@@ -266,7 +250,6 @@ unsigned read_datalog(char const * file) {
             original_rules, 
             rules_code,
             ex_ctx,
-            s_params,
             true);
         return ERR_MEMOUT;
     }
diff --git a/src/shell/datalog_frontend.h b/src/shell/datalog_frontend.h
index e53e35c89..8022d5046 100644
--- a/src/shell/datalog_frontend.h
+++ b/src/shell/datalog_frontend.h
@@ -19,11 +19,6 @@ Revision History:
 #ifndef _DATALOG_FRONTEND_H_
 #define _DATALOG_FRONTEND_H_
 
-struct datalog_params {
-    symbol m_default_table;
-    bool   m_default_table_checked;
-    datalog_params();
-};
 
 unsigned read_datalog(char const * file);
 
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 63e604719..e0fa4a1f2 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -27,8 +27,8 @@ Revision History:
 #include"z3_log_frontend.h"
 #include"warning.h"
 #include"version.h"
-#include"datalog_frontend.h"
 #include"dimacs_frontend.h"
+#include"datalog_frontend.h"
 #include"timeout.h"
 #include"z3_exception.h"
 #include"error_codes.h"