diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp
index a75e908d38c..cc177090a0d 100644
--- a/src/analyses/invariant_propagation.cpp
+++ b/src/analyses/invariant_propagation.cpp
@@ -191,8 +191,6 @@ bool invariant_propagationt::check_type(const typet &type) const
     return false;
   else if(type.id()==ID_array)
     return false;
-  else if(type.id() == ID_symbol_type)
-    return check_type(ns.follow(type));
   else if(type.id()==ID_unsignedbv ||
           type.id()==ID_signedbv)
     return true;
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 0337772d696..bc58d707e89 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -415,8 +415,6 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
        to_array_type(final_new).size().is_not_nil() &&
        final_old.subtype()==final_new.subtype())
     {
-      // we don't do symbol types for arrays anymore
-      PRECONDITION(old_symbol.type.id() != ID_symbol_type);
       old_symbol.type=new_symbol.type;
     }
     else if(
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index bed63ec7de9..a5c42d0bf42 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -504,7 +504,6 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
     const typet &type=designator.back().subtype;
     const typet &full_type=follow(type);
-    CHECK_RETURN(full_type.id() != ID_symbol_type);
 
     // do we initialize a scalar?
     if(full_type.id()!=ID_struct &&
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 41c79d2d7c1..a00ee818d62 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -440,43 +440,6 @@ std::string expr2ct::convert_rec(
   {
     return convert_array_type(src, qualifiers, declarator);
   }
-  else if(src.id() == ID_symbol_type)
-  {
-    symbol_typet symbolic_type=to_symbol_type(src);
-    const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
-
-    // Providing we have a valid identifer, we can just use that rather than
-    // trying to find the concrete type
-    if(typedef_identifer!="")
-    {
-      return q+id2string(typedef_identifer)+d;
-    }
-    else
-    {
-      const typet &followed=ns.follow(src);
-
-      if(followed.id()==ID_struct)
-      {
-        std::string dest=q+"struct";
-        const irep_idt &tag=to_struct_type(followed).get_tag();
-        if(tag!="")
-          dest+=" "+id2string(tag);
-        dest+=d;
-        return dest;
-      }
-      else if(followed.id()==ID_union)
-      {
-        std::string dest=q+"union";
-        const irep_idt &tag=to_union_type(followed).get_tag();
-        if(tag!="")
-          dest+=" "+id2string(tag);
-        dest+=d;
-        return dest;
-      }
-      else
-        return convert_rec(followed, new_qualifiers, declarator);
-    }
-  }
   else if(src.id()==ID_struct_tag)
   {
     const struct_tag_typet &struct_tag_type=
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index 2c8502703da..509de428a97 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -894,7 +894,6 @@ void cpp_typecheckt::typecheck_friend_declaration(
 
     // TODO
     //    typecheck_type(ftype);
-    //    assert(ftype.id()==ID_symbol_type);
     //    symbol.type.add("ID_C_friends").move_to_sub(ftype);
 
     return;
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index e17e2e783e5..a4ab37a4d6e 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -442,8 +442,8 @@ void cpp_typecheckt::check_member_initializers(
       for(const auto &b : bases)
       {
         if(
-          to_symbol_type(member_type).get_identifier() ==
-          to_symbol_type(b.type()).get_identifier())
+          to_struct_tag_type(member_type).get_identifier() ==
+          to_struct_tag_type(b.type()).get_identifier())
         {
           ok=true;
           break;
@@ -483,14 +483,15 @@ void cpp_typecheckt::check_member_initializers(
         if(c.type().id() != ID_struct_tag)
           continue;
 
-        const symbolt &symb = lookup(to_symbol_type(c.type()).get_identifier());
+        const symbolt &symb =
+          lookup(to_struct_tag_type(c.type()).get_identifier());
         if(symb.type.id()!=ID_struct)
           break;
 
         // check for a direct parent
         for(const auto &b : bases)
         {
-          if(symb.name == to_symbol_type(b.type()).get_identifier())
+          if(symb.name == to_struct_tag_type(b.type()).get_identifier())
           {
             ok=true;
             break;
@@ -513,7 +514,7 @@ void cpp_typecheckt::check_member_initializers(
         {
           if(
             member_type.get(ID_identifier) ==
-            to_symbol_type(b.type()).get_identifier())
+            to_struct_tag_type(b.type()).get_identifier())
           {
             ok=true;
             break;
@@ -638,8 +639,8 @@ void cpp_typecheckt::full_member_initialization(
           break;
 
         if(
-          to_symbol_type(b.type()).get_identifier() ==
-          to_symbol_type(member_type).get_identifier())
+          to_struct_tag_type(b.type()).get_identifier() ==
+          to_struct_tag_type(member_type).get_identifier())
         {
           final_initializers.move_to_sub(initializer);
           found=true;
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
index b4dadc6422d..22f5bf112ba 100644
--- a/src/cpp/cpp_typecheck_template.cpp
+++ b/src/cpp/cpp_typecheck_template.cpp
@@ -808,7 +808,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
 
     if(cpp_declarator_converter.is_typedef)
     {
-      parameter = exprt(ID_type, symbol_typet(symbol.name));
+      parameter = exprt(ID_type, struct_tag_typet(symbol.name));
       parameter.type().add_source_location()=declaration.find_location();
     }
     else
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 77aa0c4d2e9..34fae6f31ce 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -61,10 +61,10 @@ void dump_ct::operator()(std::ostream &os)
     {
       typet &type=it2->type();
 
-      if(type.id() == ID_symbol_type && type.get_bool(ID_C_transparent_union))
+      if(type.id() == ID_union_tag && type.get_bool(ID_C_transparent_union))
       {
-        symbolt new_type_sym=
-          ns.lookup(to_symbol_type(type).get_identifier());
+        symbolt new_type_sym =
+          ns.lookup(to_union_tag_type(type).get_identifier());
 
         new_type_sym.name=id2string(new_type_sym.name)+"$transparent";
         new_type_sym.type.set(ID_C_transparent_union, true);
@@ -72,7 +72,7 @@ void dump_ct::operator()(std::ostream &os)
         // we might have it already, in which case this has no effect
         symbols_transparent.add(new_type_sym);
 
-        to_symbol_type(type).set_identifier(new_type_sym.name);
+        to_union_tag_type(type).set_identifier(new_type_sym.name);
         type.remove(ID_C_transparent_union);
       }
     }
@@ -181,9 +181,16 @@ void dump_ct::operator()(std::ostream &os)
 
         if(type_id==ID_c_enum)
           convert_compound_enum(symbol.type, global_decl_stream);
+        else if(type_id == ID_struct)
+        {
+          global_decl_stream << type_to_string(struct_tag_typet{symbol.name})
+                             << ";\n\n";
+        }
         else
-          global_decl_stream << type_to_string(symbol_typet(symbol.name))
+        {
+          global_decl_stream << type_to_string(union_tag_typet{symbol.name})
                              << ";\n\n";
+        }
       }
     }
     else if(symbol.is_static_lifetime && symbol.type.id()!=ID_code)
@@ -297,10 +304,12 @@ void dump_ct::convert_compound_declaration(
     return;
 
   // do compound type body
-  if(symbol.type.id()==ID_struct ||
-     symbol.type.id()==ID_union ||
-     symbol.type.id()==ID_c_enum)
-    convert_compound(symbol.type, symbol_typet(symbol.name), true, os_body);
+  if(symbol.type.id() == ID_struct)
+    convert_compound(symbol.type, struct_tag_typet(symbol.name), true, os_body);
+  else if(symbol.type.id() == ID_union)
+    convert_compound(symbol.type, union_tag_typet(symbol.name), true, os_body);
+  else if(symbol.type.id() == ID_c_enum)
+    convert_compound(symbol.type, c_enum_tag_typet(symbol.name), true, os_body);
 }
 
 void dump_ct::convert_compound(
@@ -309,16 +318,7 @@ void dump_ct::convert_compound(
   bool recursive,
   std::ostream &os)
 {
-  if(type.id() == ID_symbol_type)
-  {
-    const symbolt &symbol=
-      ns.lookup(to_symbol_type(type).get_identifier());
-    DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
-
-    if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
-      convert_compound(symbol.type, unresolved, recursive, os);
-  }
-  else if(
+  if(
     type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
     type.id() == ID_union_tag)
   {
@@ -346,7 +346,13 @@ void dump_ct::convert_compound(
           it!=syms.end();
           ++it)
       {
-        symbol_typet s_type(*it);
+        const symbolt &type_symbol = ns.lookup(*it);
+        irep_idt tag_kind =
+          type_symbol.type.id() == ID_c_enum
+            ? ID_c_enum_tag
+            : (type_symbol.type.id() == ID_union ? ID_union_tag
+                                                 : ID_struct_tag);
+        tag_typet s_type(tag_kind, *it);
         convert_compound(s_type, s_type, recursive, os);
       }
     }
@@ -378,7 +384,7 @@ void dump_ct::convert_compound(
     UNREACHABLE;
     /*
     assert(parent_it->id() == ID_base);
-    assert(parent_it->get(ID_type) == ID_symbol_type);
+    assert(parent_it->get(ID_type) == ID_struct_tag);
 
     const irep_idt &base_id=
       parent_it->find(ID_type).get(ID_identifier);
@@ -657,12 +663,6 @@ void dump_ct::collect_typedefs_rec(
   {
     collect_typedefs_rec(type.subtype(), early, local_deps);
   }
-  else if(type.id() == ID_symbol_type)
-  {
-    const symbolt &symbol=
-      ns.lookup(to_symbol_type(type).get_identifier());
-    collect_typedefs_rec(symbol.type, early, local_deps);
-  }
   else if(
     type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
     type.id() == ID_union_tag)
@@ -1183,7 +1183,11 @@ void dump_ct::insert_local_type_decls(
     // a comment block ...
     std::ostringstream os_body;
     os_body << *it << " */\n";
-    convert_compound(type, symbol_typet(*it), false, os_body);
+    irep_idt tag_kind =
+      type.id() == ID_c_enum
+        ? ID_c_enum_tag
+        : (type.id() == ID_union ? ID_union_tag : ID_struct_tag);
+    convert_compound(type, tag_typet(tag_kind, *it), false, os_body);
     os_body << "/*";
 
     code_skipt skip;
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index c4224ff1637..02ede9f4380 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -1410,31 +1410,22 @@ goto_programt::const_targett goto_program2codet::convert_catch(
 
 void goto_program2codet::add_local_types(const typet &type)
 {
-  if(type.id() == ID_symbol_type)
+  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
   {
     const typet &full_type=ns.follow(type);
 
-    if(full_type.id()==ID_pointer ||
-       full_type.id()==ID_array)
-    {
-      add_local_types(full_type.subtype());
-    }
-    else if(full_type.id()==ID_struct ||
-            full_type.id()==ID_union)
-    {
-      const irep_idt &identifier=to_symbol_type(type).get_identifier();
-      const symbolt &symbol=ns.lookup(identifier);
+    const irep_idt &identifier = to_tag_type(type).get_identifier();
+    const symbolt &symbol = ns.lookup(identifier);
 
-      if(symbol.location.get_function().empty() ||
-         !type_names_set.insert(identifier).second)
-        return;
+    if(
+      symbol.location.get_function().empty() ||
+      !type_names_set.insert(identifier).second)
+      return;
 
-      for(const auto &c : to_struct_union_type(full_type).components())
-        add_local_types(c.type());
+    for(const auto &c : to_struct_union_type(full_type).components())
+      add_local_types(c.type());
 
-      assert(!identifier.empty());
-      type_names.push_back(identifier);
-    }
+    type_names.push_back(identifier);
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -1633,9 +1624,9 @@ void goto_program2codet::remove_const(typet &type)
   if(type.get_bool(ID_C_constant))
     type.remove(ID_C_constant);
 
-  if(type.id() == ID_symbol_type)
+  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
   {
-    const irep_idt &identifier=to_symbol_type(type).get_identifier();
+    const irep_idt &identifier = to_tag_type(type).get_identifier();
     if(!const_removed.insert(identifier).second)
       return;
 
@@ -1833,8 +1824,9 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
     if(no_typecast)
       return;
 
-    DATA_INVARIANT(expr.type().id() == ID_symbol_type,
-                   "type of union/struct expressions");
+    DATA_INVARIANT(
+      expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag,
+      "union/struct expressions should have a tag type");
 
     const typet &t=expr.type();
 
diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp
index 142f4b7e7f9..d11ac4f5b72 100644
--- a/src/goto-instrument/nondet_volatile.cpp
+++ b/src/goto-instrument/nondet_volatile.cpp
@@ -16,19 +16,16 @@ Date: September 2011
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
-bool is_volatile(
-  const symbol_tablet &symbol_table,
-  const typet &src)
+static bool is_volatile(const namespacet &ns, const typet &src)
 {
   if(src.get_bool(ID_C_volatile))
     return true;
 
-  if(src.id()==ID_symbol)
+  if(
+    src.id() == ID_struct_tag || src.id() == ID_union_tag ||
+    src.id() == ID_c_enum_tag)
   {
-    symbol_tablet::symbolst::const_iterator s_it=
-      symbol_table.symbols.find(to_symbol_type(src).get_identifier());
-    assert(s_it!=symbol_table.symbols.end());
-    return is_volatile(symbol_table, s_it->second.type);
+    return is_volatile(ns, ns.follow(src));
   }
 
   return false;
@@ -42,7 +39,8 @@ void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
   if(expr.id()==ID_symbol ||
      expr.id()==ID_dereference)
   {
-    if(is_volatile(symbol_table, expr.type()))
+    const namespacet ns(symbol_table);
+    if(is_volatile(ns, expr.type()))
     {
       typet t=expr.type();
       t.remove(ID_C_volatile);
diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp
index 00bf2653f1b..e3db31ec351 100644
--- a/src/goto-programs/destructor.cpp
+++ b/src/goto-programs/destructor.cpp
@@ -19,9 +19,9 @@ code_function_callt get_destructor(
   const namespacet &ns,
   const typet &type)
 {
-  if(type.id() == ID_symbol_type)
+  if(type.id() == ID_struct_tag)
   {
-    return get_destructor(ns, ns.follow(type));
+    return get_destructor(ns, ns.follow_tag(to_struct_tag_type(type)));
   }
   else if(type.id()==ID_struct)
   {
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index be2ef19df7a..de9b5ad11c4 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -1030,9 +1030,9 @@ mp_integer interpretert::get_size(const typet &type)
     }
     return subtype_size;
   }
-  else if(type.id() == ID_symbol_type || type.id() == ID_struct_tag)
+  else if(type.id() == ID_struct_tag)
   {
-    return get_size(ns.follow(type));
+    return get_size(ns.follow_tag(to_struct_tag_type(type)));
   }
 
   return 1;
diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp
index 161ffcc63d2..ceab31ce611 100644
--- a/src/goto-programs/json_expr.cpp
+++ b/src/goto-programs/json_expr.cpp
@@ -97,9 +97,6 @@ static exprt simplify_json_expr(const exprt &src)
 /// \return a json object
 json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
 {
-  if(type.id() == ID_symbol_type)
-    return json(ns.follow(type), ns, mode);
-
   json_objectt result;
 
   if(type.id() == ID_unsignedbv)
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
index 0d419150429..b3dacf2e9aa 100644
--- a/src/goto-programs/xml_expr.cpp
+++ b/src/goto-programs/xml_expr.cpp
@@ -25,9 +25,6 @@ Author: Daniel Kroening
 
 xmlt xml(const typet &type, const namespacet &ns)
 {
-  if(type.id() == ID_symbol_type)
-    return xml(ns.follow(type), ns);
-
   xmlt result;
 
   if(type.id() == ID_unsignedbv)
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index e341c6c89f5..4b51e662ef8 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -595,7 +595,6 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
       if(
-        member_expr.struct_op().type().id() != ID_symbol_type &&
         member_expr.struct_op().type().id() != ID_struct_tag &&
         member_expr.struct_op().type().id() != ID_union_tag)
       {
@@ -656,11 +655,6 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
   {
     return requires_renaming(to_pointer_type(type).subtype(), ns);
   }
-  else if(type.id() == ID_symbol_type)
-  {
-    const symbolt &symbol = ns.lookup(to_symbol_type(type));
-    return requires_renaming(symbol.type, ns);
-  }
   else if(type.id() == ID_union_tag)
   {
     const symbolt &symbol = ns.lookup(to_union_tag_type(type));
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index a733fec89aa..f22b85fcef1 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -58,9 +58,7 @@ static const typet &follow_tags_symbols(
   const namespacet &ns,
   const typet &type)
 {
-  if(type.id() == ID_symbol_type)
-    return ns.follow(type);
-  else if(type.id()==ID_c_enum_tag)
+  if(type.id() == ID_c_enum_tag)
     return ns.follow_tag(to_c_enum_tag_type(type));
   else if(type.id()==ID_struct_tag)
     return ns.follow_tag(to_struct_tag_type(type));
@@ -796,10 +794,10 @@ bool linkingt::adjust_object_type_rec(
     return false;
 
   if(
-    t1.id() == ID_symbol_type || t1.id() == ID_struct_tag ||
-    t1.id() == ID_union_tag || t1.id() == ID_c_enum_tag)
+    t1.id() == ID_struct_tag || t1.id() == ID_union_tag ||
+    t1.id() == ID_c_enum_tag)
   {
-    const irep_idt &identifier=t1.get(ID_identifier);
+    const irep_idt &identifier = to_tag_type(t1).get_identifier();
 
     if(info.o_symbols.insert(identifier).second)
     {
@@ -813,10 +811,10 @@ bool linkingt::adjust_object_type_rec(
     return false;
   }
   else if(
-    t2.id() == ID_symbol_type || t2.id() == ID_struct_tag ||
-    t2.id() == ID_union_tag || t2.id() == ID_c_enum_tag)
+    t2.id() == ID_struct_tag || t2.id() == ID_union_tag ||
+    t2.id() == ID_c_enum_tag)
   {
-    const irep_idt &identifier=t2.get(ID_identifier);
+    const irep_idt &identifier = to_tag_type(t2).get_identifier();
 
     if(info.n_symbols.insert(identifier).second)
     {
diff --git a/src/pointer-analysis/value_set_analysis_fi.cpp b/src/pointer-analysis/value_set_analysis_fi.cpp
index badb1ac1085..c6b59e41986 100644
--- a/src/pointer-analysis/value_set_analysis_fi.cpp
+++ b/src/pointer-analysis/value_set_analysis_fi.cpp
@@ -190,7 +190,7 @@ bool value_set_analysis_fit::check_type(const typet &type)
   }
   else if(type.id()==ID_array)
     return check_type(type.subtype());
-  else if(type.id() == ID_symbol_type)
+  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
     return check_type(ns.follow(type));
 
   return false;
diff --git a/src/pointer-analysis/value_set_analysis_fivr.cpp b/src/pointer-analysis/value_set_analysis_fivr.cpp
index 2b6cb89be8f..74924dc12c4 100644
--- a/src/pointer-analysis/value_set_analysis_fivr.cpp
+++ b/src/pointer-analysis/value_set_analysis_fivr.cpp
@@ -178,7 +178,7 @@ bool value_set_analysis_fivrt::check_type(const typet &type)
   }
   else if(type.id()==ID_array)
     return check_type(type.subtype());
-  else if(type.id() == ID_symbol_type)
+  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
     return check_type(ns.follow(type));
 
   return false;
diff --git a/src/pointer-analysis/value_set_analysis_fivrns.cpp b/src/pointer-analysis/value_set_analysis_fivrns.cpp
index 8712654b9ab..0b22b315c96 100644
--- a/src/pointer-analysis/value_set_analysis_fivrns.cpp
+++ b/src/pointer-analysis/value_set_analysis_fivrns.cpp
@@ -178,8 +178,6 @@ bool value_set_analysis_fivrnst::check_type(const typet &type)
     }
     else if(type.id()==ID_array)
       return check_type(type.subtype());
-    else if(type.id() == ID_symbol_type)
-      return check_type(ns.follow(type));
 
   return false;
 }
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 6f7dea334a6..ba7c66af987 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -180,8 +180,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   }
   else if(type_id==ID_pointer)
     entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
-  else if(type_id == ID_symbol_type)
-    entry=get_entry(ns.follow(type));
   else if(type_id==ID_struct_tag)
     entry=get_entry(ns.follow_tag(to_struct_tag_type(type)));
   else if(type_id==ID_union_tag)
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
index 73ed1e41f85..27dd087f554 100644
--- a/src/solvers/flattening/boolbv_with.cpp
+++ b/src/solvers/flattening/boolbv_with.cpp
@@ -100,8 +100,6 @@ void boolbvt::convert_with(
   else if(type.id() == ID_union_tag)
     return convert_with(
       ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
-  else if(type.id() == ID_symbol_type)
-    return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);
 
   error().source_location=type.source_location();
   error() << "unexpected with type: " << type.id() << eom;
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 971389f57f6..24ea918c7c9 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -3916,9 +3916,6 @@ void smt2_convt::unflatten(
   const typet &type,
   unsigned nesting)
 {
-  if(type.id() == ID_symbol_type)
-    return unflatten(where, ns.follow(type));
-
   if(type.id()==ID_bool)
   {
     if(where==wheret::BEGIN)
@@ -4444,8 +4441,6 @@ void smt2_convt::convert_type(const typet &type)
     out << "Real";
   else if(type.id()==ID_integer)
     out << "Int";
-  else if(type.id() == ID_symbol_type)
-    convert_type(ns.follow(type));
   else if(type.id()==ID_complex)
   {
     if(use_datatypes)
@@ -4657,17 +4652,6 @@ void smt2_convt::find_symbols_rec(
   {
     find_symbols_rec(type.subtype(), recstack);
   }
-  else if(type.id() == ID_symbol_type)
-  {
-    const symbol_typet &st=to_symbol_type(type);
-    const irep_idt &id=st.get_identifier();
-
-    if(recstack.find(id)==recstack.end())
-    {
-      recstack.insert(id);
-      find_symbols_rec(ns.follow(type), recstack);
-    }
-  }
   else if(type.id() == ID_struct_tag)
   {
     const auto &struct_tag = to_struct_tag_type(type);
diff --git a/src/util/README.md b/src/util/README.md
index 52432e42b42..a35bd292ad6 100644
--- a/src/util/README.md
+++ b/src/util/README.md
@@ -104,10 +104,10 @@ stored in two [sub](\ref irept::dt::sub)s named “subtype” (a single type) an
 “subtypes” (a vector of types). For pre-defined types see `std_types.h` and
 `mathematical_types.h`.
 
-\subsubsection symbol_typet_section symbol_typet
+\subsubsection tag_typet_section tag_typet
 
-\ref symbol_typet is a type used to store a reference to the symbol table. The
-full \ref symbolt can be retrieved using the identifier of \ref symbol_typet.
+\ref tag_typet is a type used to store a reference to the symbol table. The
+full \ref symbolt can be retrieved using the identifier of \ref tag_typet.
 
 \subsection exprt_section exprt
 
@@ -174,7 +174,7 @@ Local variables' symbol values are always ignored;
 any initialiser must be explicitly assigned after they are instantiated by a
 declaration (\ref code_declt).
 
-Symbol expressions (\ref symbol_exprt) and types (\ref symbol_typet) refer to
+Symbol expressions (\ref symbol_exprt) and types (\ref tag_typet) refer to
 symbols stored in a symbol table. Symbol expressions can be thought of as
 referring to the table for more detail about a symbol (for example, is it a
 local or a global variable, or perhaps a function?), and have a type which must
@@ -198,8 +198,8 @@ found. Note class \ref multi_namespacet can layer arbitrary numbers of symbol
 tables, while for historical reasons \ref namespacet can layer up to two.
 
 The namespace wrapper class also provides the \ref namespacet::follow
-operation, which dereferences a `symbol_typet` to retrieve the type it refers
-to, including following a symbol_typet which refers to another symbol which
+operation, which dereferences a `tag_typet` to retrieve the type it refers
+to, including following a type tag which refers to another symbol which
 eventually refers to a 'real' type.
 
 \subsubsection symbolt_lifetime Symbol lifetimes
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
index d98af3c5f9d..07fa6da5af9 100644
--- a/src/util/base_type.cpp
+++ b/src/util/base_type.cpp
@@ -53,20 +53,7 @@ class base_type_eqt
 void base_type_rec(
   typet &type, const namespacet &ns, std::set<irep_idt> &symb)
 {
-  if(type.id() == ID_symbol_type)
-  {
-    const symbolt *symbol;
-
-    if(
-      !ns.lookup(to_symbol_type(type).get_identifier(), symbol) &&
-      symbol->is_type && !symbol->type.is_nil())
-    {
-      type = symbol->type;
-      base_type_rec(type, ns, symb); // recursive call
-      return;
-    }
-  }
-  else if(
+  if(
     type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
     type.id() == ID_union_tag)
   {
@@ -99,20 +86,7 @@ void base_type_rec(
     typet &subtype=to_pointer_type(type).subtype();
 
     // we need to avoid running into an infinite loop
-    if(subtype.id() == ID_symbol_type)
-    {
-      const irep_idt &id = to_symbol_type(subtype).get_identifier();
-
-      if(symb.find(id) != symb.end())
-        return;
-
-      symb.insert(id);
-
-      base_type_rec(subtype, ns, symb);
-
-      symb.erase(id);
-    }
-    else if(
+    if(
       subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag ||
       subtype.id() == ID_union_tag)
     {
@@ -160,8 +134,8 @@ bool base_type_eqt::base_type_eq_rec(
 
   // loop avoidance
   if(
-    (type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
-     type1.id() == ID_struct_tag || type1.id() == ID_union_tag) &&
+    (type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
+     type1.id() == ID_union_tag) &&
     type2.id() == type1.id())
   {
     // already in same set?
@@ -172,8 +146,8 @@ bool base_type_eqt::base_type_eq_rec(
   }
 
   if(
-    type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
-    type1.id() == ID_struct_tag || type1.id() == ID_union_tag)
+    type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
+    type1.id() == ID_union_tag)
   {
     const symbolt &symbol=
       ns.lookup(type1.get(ID_identifier));
@@ -185,8 +159,8 @@ bool base_type_eqt::base_type_eq_rec(
   }
 
   if(
-    type2.id() == ID_symbol_type || type2.id() == ID_c_enum_tag ||
-    type2.id() == ID_struct_tag || type2.id() == ID_union_tag)
+    type2.id() == ID_c_enum_tag || type2.id() == ID_struct_tag ||
+    type2.id() == ID_union_tag)
   {
     const symbolt &symbol=
       ns.lookup(type2.get(ID_identifier));
@@ -309,9 +283,8 @@ bool base_type_eqt::base_type_eq_rec(
 /// Check types for equality across all levels of hierarchy. For equality
 /// in the top level of the hierarchy only use \ref type_eq.
 /// Example:
-/// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal,
-/// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a")
-///   .type}` will also compare equal.
+/// - `struct_typet {union_tag_typet("a")}` and `struct_typet {ns.lookup("a")
+///   .type}` will compare equal.
 /// \param type1: The first type to compare.
 /// \param type2: The second type to compare.
 /// \param ns: The namespace, needed for resolution of symbols.
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
index 6829d1384f6..25c419a386c 100644
--- a/src/util/endianness_map.cpp
+++ b/src/util/endianness_map.cpp
@@ -51,9 +51,7 @@ void endianness_mapt::build_little_endian(const typet &src)
 
 void endianness_mapt::build_big_endian(const typet &src)
 {
-  if(src.id() == ID_symbol_type)
-    build_big_endian(ns.follow(src));
-  else if(src.id()==ID_c_enum_tag)
+  if(src.id() == ID_c_enum_tag)
     build_big_endian(ns.follow_tag(to_c_enum_tag_type(src)));
   else if(src.id()==ID_unsignedbv ||
           src.id()==ID_signedbv ||
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index b7c3cd07125..2895fce9eb0 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -261,19 +261,6 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
       return std::move(value);
     }
   }
-  else if(type_id == ID_symbol_type)
-  {
-    auto result = expr_initializer_rec(ns.follow(type), source_location);
-
-    if(!result.has_value())
-      return {};
-
-    // we might have mangled the type for arrays, so keep that
-    if(type.id() != ID_array)
-      result->type() = type;
-
-    return *result;
-  }
   else if(type_id==ID_c_enum_tag)
   {
     auto result = expr_initializer_rec(
diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp
index 6efc7c41c77..afde421f333 100644
--- a/src/util/find_symbols.cpp
+++ b/src/util/find_symbols.cpp
@@ -156,8 +156,6 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
       //  dest.insert(identifier);
     }
   }
-  else if(src.id() == ID_symbol_type)
-    dest.insert(to_symbol_type(src).get_identifier());
   else if(src.id()==ID_array)
   {
     // do the size -- the subtype is already done
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
index 54cbfe2a264..5b656d81312 100644
--- a/src/util/format_type.cpp
+++ b/src/util/format_type.cpp
@@ -79,8 +79,6 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
     return os << "struct " << to_struct_tag_type(type).get_identifier();
   else if(id == ID_c_enum_tag)
     return os << "c_enum " << to_c_enum_tag_type(type).get_identifier();
-  else if(id == ID_symbol_type)
-    return os << "symbol_type " << to_symbol_type(type).get_identifier();
   else if(id == ID_signedbv)
     return os << "signedbv[" << to_signedbv_type(type).get_width() << ']';
   else if(id == ID_unsignedbv)
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 17554082981..a07b4a25c83 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -57,7 +57,6 @@ IREP_ID_ONE(bitxnor)
 IREP_ID_ONE(notequal)
 IREP_ID_ONE(if)
 IREP_ID_ONE(symbol)
-IREP_ID_ONE(symbol_type)
 IREP_ID_ONE(next_symbol)
 IREP_ID_ONE(nondet_symbol)
 IREP_ID_ONE(predicate_symbol)
diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp
index c0bcc910731..827d59fdc09 100644
--- a/src/util/namespace.cpp
+++ b/src/util/namespace.cpp
@@ -34,17 +34,6 @@ const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const
   return lookup(expr.get_identifier());
 }
 
-/// Generic lookup function for a symbol type in a symbol table.
-/// \param type: The symbol type to lookup.
-/// \return The symbol found in the namespace.
-/// \remarks The lookup function called assumes that the type symbol we are
-/// looking for exists in the symbol table. If it doesn't, it hits an
-/// INVARIANT.
-const symbolt &namespace_baset::lookup(const symbol_typet &type) const
-{
-  return lookup(type.get_identifier());
-}
-
 /// Generic lookup function for a tag type in a symbol table.
 /// \param type: The tag type to lookup.
 /// \return The symbol found in the namespace.
@@ -67,21 +56,7 @@ const typet &namespace_baset::follow(const typet &src) const
   if(src.id() == ID_struct_tag)
     return follow_tag(to_struct_tag_type(src));
 
-  if(src.id() != ID_symbol_type)
-    return src;
-
-  const symbolt *symbol = &lookup(to_symbol_type(src));
-
-  // let's hope it's not cyclic...
-  while(true)
-  {
-    DATA_INVARIANT(symbol->is_type, "symbol type points to type");
-
-    if(symbol->type.id() == ID_symbol_type)
-      symbol = &lookup(to_symbol_type(symbol->type));
-    else
-      return symbol->type;
-  }
+  return src;
 }
 
 /// Follow type tag of union type.
diff --git a/src/util/namespace.h b/src/util/namespace.h
index 87dc00d528b..da665bd939c 100644
--- a/src/util/namespace.h
+++ b/src/util/namespace.h
@@ -18,7 +18,6 @@ class exprt;
 class symbolt;
 class typet;
 class symbol_exprt;
-class symbol_typet;
 class tag_typet;
 class union_typet;
 class struct_typet;
@@ -55,7 +54,6 @@ class namespace_baset
   }
 
   const symbolt &lookup(const symbol_exprt &) const;
-  const symbolt &lookup(const symbol_typet &) const;
   const symbolt &lookup(const tag_typet &) const;
 
   virtual ~namespace_baset();
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index d3a5c0d8154..fa1f8ac47bb 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -203,10 +203,6 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
 
     return mp_integer(to_bitvector_type(type).get_width());
   }
-  else if(type.id() == ID_symbol_type)
-  {
-    return pointer_offset_bits(ns.follow(type), ns);
-  }
   else if(type.id() == ID_union_tag)
   {
     return pointer_offset_bits(ns.follow_tag(to_union_tag_type(type)), ns);
@@ -503,10 +499,6 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       bytes++;
     return from_integer(bytes, size_type());
   }
-  else if(type.id() == ID_symbol_type)
-  {
-    return size_of_expr(ns.follow(type), ns);
-  }
   else if(type.id() == ID_union_tag)
   {
     return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns);
diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
index 26dbe33cf79..0c312dc4689 100644
--- a/src/util/rename_symbol.cpp
+++ b/src/util/rename_symbol.cpp
@@ -161,17 +161,6 @@ bool rename_symbolt::rename(typet &dest) const
       }
     }
   }
-  else if(dest.id() == ID_symbol_type)
-  {
-    type_mapt::const_iterator it=
-      type_map.find(to_symbol_type(dest).get_identifier());
-
-    if(it!=type_map.end())
-    {
-      to_symbol_type(dest).set_identifier(it->second);
-      result=false;
-    }
-  }
   else if(dest.id()==ID_c_enum_tag ||
           dest.id()==ID_struct_tag ||
           dest.id()==ID_union_tag)
@@ -233,11 +222,6 @@ bool rename_symbolt::have_to_rename(const typet &dest) const
         return true;
     }
   }
-  else if(dest.id() == ID_symbol_type)
-  {
-    const irep_idt &identifier = to_symbol_type(dest).get_identifier();
-    return type_map.find(identifier) != type_map.end();
-  }
   else if(dest.id()==ID_c_enum_tag ||
           dest.id()==ID_struct_tag ||
           dest.id()==ID_union_tag)
diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp
index 19b2f49dc7e..2b391db5b04 100644
--- a/src/util/std_types.cpp
+++ b/src/util/std_types.cpp
@@ -262,9 +262,7 @@ bool is_constant_or_has_constant_components(
   // we have to use the namespace to resolve to its definition:
   // struct t { const int a; };
   // struct t t1;
-  if(type.id() == ID_symbol_type ||
-     type.id() == ID_struct_tag ||
-     type.id() == ID_union_tag)
+  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
   {
     const auto &resolved_type = ns.follow(type);
     return has_constant_components(resolved_type);
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 1fe6c0c8f4a..a42b29f9283 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -54,56 +54,6 @@ class empty_typet:public typet
   }
 };
 
-/// A reference into the symbol table
-class symbol_typet:public typet
-{
-public:
-  explicit symbol_typet(const irep_idt &identifier) : typet(ID_symbol_type)
-  {
-    set_identifier(identifier);
-  }
-
-  void set_identifier(const irep_idt &identifier)
-  {
-    set(ID_identifier, identifier);
-  }
-
-  const irep_idt &get_identifier() const
-  {
-    return get(ID_identifier);
-  }
-};
-
-/// Check whether a reference to a typet is a \ref symbol_typet.
-/// \param type: Source type.
-/// \return True if \p type is a \ref symbol_typet.
-template <>
-inline bool can_cast_type<symbol_typet>(const typet &type)
-{
-  return type.id() == ID_symbol_type;
-}
-
-/// \brief Cast a typet to a \ref symbol_typet.
-///
-/// This is an unchecked conversion. \a type must be known to be
-/// \ref symbol_typet. Will fail with a precondition violation if type
-/// doesn't match.
-///
-/// \param type: Source type.
-/// \return Object of type \ref symbol_typet.
-inline const symbol_typet &to_symbol_type(const typet &type)
-{
-  PRECONDITION(can_cast_type<symbol_typet>(type));
-  return static_cast<const symbol_typet &>(type);
-}
-
-/// \copydoc to_symbol_type(const typet &)
-inline symbol_typet &to_symbol_type(typet &type)
-{
-  PRECONDITION(can_cast_type<symbol_typet>(type));
-  return static_cast<symbol_typet &>(type);
-}
-
 /// Base type for structs and unions
 ///
 /// For example C structs, C unions, C++ classes, Java classes.
diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp
index 6ba8036d487..efc02e5c282 100644
--- a/src/util/type_eq.cpp
+++ b/src/util/type_eq.cpp
@@ -33,19 +33,5 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
   if(type1==type2)
     return true;
 
-  if(const auto symbol_type1 = type_try_dynamic_cast<symbol_typet>(type1))
-  {
-    const symbolt &symbol = ns.lookup(*symbol_type1);
-    CHECK_RETURN(symbol.is_type);
-    return type_eq(symbol.type, type2, ns);
-  }
-
-  if(const auto symbol_type2 = type_try_dynamic_cast<symbol_typet>(type2))
-  {
-    const symbolt &symbol = ns.lookup(*symbol_type2);
-    CHECK_RETURN(symbol.is_type);
-    return type_eq(type1, symbol.type, ns);
-  }
-
   return false;
 }