diff --git a/examples/tui/example-battleship-1x4.limbo b/examples/tui/example-battleship-1x4.limbo
index 37ce02227d19896ee8d2d24c5ff21ee50256cc85..bddcde9b93a59a0847e0a3e54c96d0a39cca05cd 100644
--- a/examples/tui/example-battleship-1x4.limbo
+++ b/examples/tui/example-battleship-1x4.limbo
@@ -55,7 +55,8 @@ KB: water(s(tail(three)))=T
 KB: p=p1 v p=p2 v p=p3 v p=p4 v water(p)=T
 // We don't need the following in the KB. If we do have it, however,
 // split level 1 suffices for the assertions below.
-// KB: head(three)=p v body(three)=p v tail(three)=p v water(p)=T
+//KB: head(three)=p v body(three)=p v tail(three)=p v water(p)=T
+Assert: Fa p K<2> (head(three)=p v body(three)=p v tail(three)=p v water(p)=T)
 Assert: Fa p G K<2> (head(three)=p v body(three)=p v tail(three)=p v water(p)=T)
 
 Call: bs_init(p1, p2, p3, p4)
diff --git a/src/limbo/format/pdl/parser.h b/src/limbo/format/pdl/parser.h
index d0f07b6d177968699c4a275d33935579bfe00984..7436ecb51be6e573c8aa211d9f729d4f8cb3a970 100644
--- a/src/limbo/format/pdl/parser.h
+++ b/src/limbo/format/pdl/parser.h
@@ -824,7 +824,7 @@ class Parser {
       Symbol::Sort sort = ctx->LookupSort(sort_id);
       std::vector<Term> ts;
       if (ts_a.empty()) {
-        Grounder::Names ns = ctx->kb().sphere(0).grounder().names(sort);
+        const KnowledgeBase::TermSet& ns = ctx->kb().mentioned_names(sort);
         ts.insert(ts.end(), ns.begin(), ns.end());
       } else {
         for (const Action<Term>& t_a : ts_a) {
diff --git a/src/limbo/grounder.h b/src/limbo/grounder.h
index e130836262c32998c826450c24b6688bfa9c058d..98407a5da33a73005a3dd204bcf33ed937fb12ce 100644
--- a/src/limbo/grounder.h
+++ b/src/limbo/grounder.h
@@ -133,10 +133,10 @@ class Grounder {
       SortedTermSet terms;
     } relevant;
     struct {
-      SortedTermSet occurring;       // names occurring in clause or prepared-for query (but are not plus-names)
+      SortedTermSet mentioned;       // names mentioned in clause or prepared-for query (but are not plus-names)
       SortedTermSet plus_max;        // plus-names that may be used for multiple purposes
       SortedTermSet plus_new;        // plus-names that may not be used for multiple purposes
-      SortedTermSet plus_occurring;  // plus-names that later occurred in formulas (which lead to plus_new names)
+      SortedTermSet plus_mentioned;  // plus-names that later occurred in formulas (which lead to plus_new names)
     } names;
     struct {
       Ungrounded<Literal>::Set ungrounded;  // literals in prepared-for query
@@ -319,7 +319,7 @@ class Grounder {
       explicit Begin(Symbol::Sort sort) : sort(sort) {}
       name_iterator operator()(const Ply& p) const {
         auto b = plus_iterator(p.names.plus_max.begin(sort), p.names.plus_max.end(sort), p.names.plus_new.begin(sort));
-        return name_iterator(p.names.occurring.begin(sort), p.names.occurring.end(sort), b);
+        return name_iterator(p.names.mentioned.begin(sort), p.names.mentioned.end(sort), b);
       }
      private:
       Symbol::Sort sort;
@@ -329,7 +329,7 @@ class Grounder {
       explicit End(Symbol::Sort sort) : sort(sort) {}
       name_iterator operator()(const Ply& p) const {
         auto e = plus_iterator(p.names.plus_max.end(sort), p.names.plus_max.end(sort), p.names.plus_new.begin(sort));
-        return name_iterator(p.names.occurring.end(sort), p.names.occurring.end(sort), e);
+        return name_iterator(p.names.mentioned.end(sort), p.names.mentioned.end(sort), e);
       }
      private:
       Symbol::Sort sort;
@@ -451,9 +451,9 @@ class Grounder {
         if (t.name()) {
           if (!IsOccurringName(t)) {
             if (IsPlusName(t)) {
-              p.names.plus_occurring.insert(t);
+              p.names.plus_mentioned.insert(t);
             } else {
-              p.names.occurring.insert(t);
+              p.names.mentioned.insert(t);
             }
           }
         }
@@ -462,7 +462,7 @@ class Grounder {
       p.clauses.ungrounded.push_back(uc);
       CreateMaxPlusNames(uc.vars, 1);
     }
-    CreateNewPlusNames(p.names.plus_occurring);
+    CreateNewPlusNames(p.names.plus_mentioned);
     p.do_not_add_if_inconsistent = do_not_add_if_inconsistent;
     const Setup::Result r = Reground();
     if (undo) {
@@ -492,9 +492,9 @@ class Grounder {
         if (t.name()) {
           if (!IsOccurringName(t)) {
             if (IsPlusName(t)) {
-              p.names.plus_occurring.insert(t);
+              p.names.plus_mentioned.insert(t);
             } else {
-              p.names.occurring.insert(t);
+              p.names.mentioned.insert(t);
             }
           }
         } else if (t.variable()) {
@@ -507,7 +507,7 @@ class Grounder {
       }
       return true;
     });
-    CreateNewPlusNames(p.names.plus_occurring);
+    CreateNewPlusNames(p.names.plus_mentioned);
     CreateMaxPlusNames(phi.n_vars());  // XXX or CreateNewPlusNames()?
     Reground();
     if (undo) {
@@ -772,7 +772,7 @@ class Grounder {
   bool IsOccurringName(Term n) const {
     assert(n.name());
     for (const Ply& p : plies_) {
-      if (p.names.occurring.contains(n) || p.names.plus_occurring.contains(n)) {
+      if (p.names.mentioned.contains(n) || p.names.plus_mentioned.contains(n)) {
         return true;
       }
     }
@@ -985,7 +985,7 @@ rescan:
     Ply& p = last_ply();
     assert(p.relevant.filter);
     assert(p.clauses.ungrounded.empty());
-    assert(p.names.occurring.all_empty() && p.names.plus_new.all_empty() && p.names.plus_max.all_empty());
+    assert(p.names.mentioned.all_empty() && p.names.plus_new.all_empty() && p.names.plus_max.all_empty());
     const Setup& old_s = p.clauses.shallow_setup.setup();
     std::unique_ptr<Setup> new_s(new Setup());
     for (size_t i : old_s.clauses()) {
diff --git a/src/limbo/kb.h b/src/limbo/kb.h
index 65e7b72ad32ece559f87b04b54276f9fc9e9af2d..992e6b368c4fd5fabe70c6af84472b54fcf4f7be 100644
--- a/src/limbo/kb.h
+++ b/src/limbo/kb.h
@@ -53,6 +53,8 @@ class KnowledgeBase {
   typedef internal::size_t size_t;
   typedef size_t sphere_index;
   typedef Formula::belief_level belief_level;
+  typedef Formula::TermSet TermSet;
+  typedef Formula::SortedTermSet SortedTermSet;
 
   KnowledgeBase(Symbol::Factory* sf, Term::Factory* tf) : sf_(sf), tf_(tf), objective_(sf, tf) {
     spheres_.emplace_back(sf, tf);
@@ -108,6 +110,9 @@ class KnowledgeBase {
   const Solver& sphere(sphere_index p) const { const_cast<KnowledgeBase&>(*this).UpdateSpheres(); return spheres_[p]; }
   const std::vector<Solver>& spheres() const { const_cast<KnowledgeBase&>(*this).UpdateSpheres(); return spheres_; }
 
+  const SortedTermSet& mentioned_names() const { return names_; }
+  const TermSet& mentioned_names(Symbol::Sort sort) const { return names_[sort]; }
+
  private:
   struct Conditional {
     belief_level k;
@@ -116,8 +121,6 @@ class KnowledgeBase {
     Clause not_ante_or_conse;
     bool assume_consistent;
   };
-  typedef Formula::TermSet TermSet;
-  typedef Formula::SortedTermSet SortedTermSet;
 
   void Add(belief_level k,
            belief_level l,