diff --git a/src/library/inductive_compiler/add_decl.cpp b/src/library/inductive_compiler/add_decl.cpp
index c8f3a85408..2ea0afacee 100644
--- a/src/library/inductive_compiler/add_decl.cpp
+++ b/src/library/inductive_compiler/add_decl.cpp
@@ -25,7 +25,7 @@ environment add_inductive_declaration(environment const & old_env, options const
 
 environment add_structure_declaration_aux(environment const & old_env, options const &, buffer <name> const & lp_names,
                                           buffer <expr> const & params, expr const & ind, expr const & intro_rule,
-                                          bool is_meta) {
+                                          bool /* is_meta */) {
     buffer<expr> inds;
     inds.push_back(ind);
 
diff --git a/src/library/inductive_compiler/ginductive.cpp b/src/library/inductive_compiler/ginductive.cpp
index ad6fdd2df9..25f48b6036 100644
--- a/src/library/inductive_compiler/ginductive.cpp
+++ b/src/library/inductive_compiler/ginductive.cpp
@@ -357,8 +357,6 @@ environment register_ginductive_decl(environment const & env, ginductive_decl co
         intro_rules.push_back(names(ir_names));
     }
     entry.m_intro_rules = to_list(intro_rules);
-    entry.m_packs = names(decl.get_packs());
-    entry.m_unpacks = names(decl.get_unpacks());
 
     entry.m_ir_offsets = to_list(decl.get_ir_offsets());
     entry.m_idx_to_ir_range = to_list(decl.get_idx_to_ir_range());
diff --git a/src/library/inductive_compiler/ginductive_decl.h b/src/library/inductive_compiler/ginductive_decl.h
index 6113c259e7..1188859861 100644
--- a/src/library/inductive_compiler/ginductive_decl.h
+++ b/src/library/inductive_compiler/ginductive_decl.h
@@ -7,7 +7,6 @@ Author: Daniel Selsam
 #pragma once
 #include "kernel/environment.h"
 #include "kernel/find_fn.h"
-#include "library/tactic/simp_lemmas.h"
 #include "library/inductive_compiler/util.h"
 
 namespace lean {
@@ -24,10 +23,6 @@ class ginductive_decl {
     buffer<unsigned>                  m_ir_offsets; // # total intro rules @ basic
     buffer<pair<unsigned, unsigned> > m_idx_to_ir_range; // # total inds @ mutual
 
-    buffer<name> m_packs;
-    buffer<name> m_unpacks;
-
-    optional<simp_lemmas> m_sizeof_lemmas;
 public:
     ginductive_decl(unsigned nest_depth, buffer<name> const & lp_names, buffer<expr> const & params,
                     buffer<unsigned> const & num_indices, buffer<unsigned> const & ir_offsets):
@@ -52,13 +47,6 @@ public:
         }
     }
 
-    void set_sizeof_lemmas(simp_lemmas const & sizeof_lemmas) {
-        m_sizeof_lemmas = optional<simp_lemmas>(sizeof_lemmas);
-    }
-
-    bool has_sizeof_lemmas() const { return static_cast<bool>(m_sizeof_lemmas); }
-    simp_lemmas get_sizeof_lemmas() const { return *m_sizeof_lemmas; }
-
     unsigned get_nest_depth() const { return m_nest_depth; }
     bool is_inner() const { return m_is_inner; }
 
@@ -92,11 +80,6 @@ public:
     buffer<pair<unsigned, unsigned> > const & get_idx_to_ir_range() const { return m_idx_to_ir_range; }
     buffer<pair<unsigned, unsigned> > & get_idx_to_ir_range() { return m_idx_to_ir_range; }
 
-    buffer<name> const & get_packs() const { return m_packs; }
-    buffer<name> & get_packs() { return m_packs; }
-    buffer<name> const & get_unpacks() const { return m_unpacks; }
-    buffer<name> & get_unpacks() { return m_unpacks; }
-
     expr mk_const(name const & n) const { return mk_constant(n, get_levels()); }
     expr mk_const_params(name const & n) const { return mk_app(mk_const(n), m_params); }
     expr get_c_ind(unsigned ind_idx) const { return mk_const(local_name(m_inds[ind_idx])); }