diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 746a01cb834..20d0a3f8566 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -253,7 +253,6 @@ bool check_c_implicit_typecast(
 typet c_typecastt::follow_with_qualifiers(const typet &src_type)
 {
   if(
-    src_type.id() != ID_symbol_type &&
     src_type.id() != ID_struct_tag &&
     src_type.id() != ID_union_tag)
   {
@@ -265,9 +264,7 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
   // collect qualifiers
   c_qualifierst qualifiers(src_type);
 
-  while(result_type.id() == ID_symbol_type ||
-        result_type.id() == ID_struct_tag ||
-        result_type.id() == ID_union_tag)
+  while(result_type.id() == ID_struct_tag || result_type.id() == ID_union_tag)
   {
     const typet &followed_type = ns.follow(result_type);
     result_type = followed_type;
@@ -350,8 +347,6 @@ c_typecastt::c_typet c_typecastt::get_c_type(
   {
     return INT;
   }
-  else if(type.id() == ID_symbol_type)
-    return get_c_type(ns.follow(type));
   else if(type.id()==ID_rational)
     return RATIONAL;
   else if(type.id()==ID_real)
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 172ac693a40..9064bc5497f 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -209,7 +209,6 @@ class c_typecheck_baset:
   virtual void typecheck_c_enum_type(typet &type);
   virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
   virtual void typecheck_code_type(code_typet &type);
-  virtual void typecheck_symbol_type(symbol_typet &type);
   virtual void typecheck_typedef_type(typet &type);
   virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
   virtual void typecheck_typeof_type(typet &type);
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 008da3b0afc..d578ec33724 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -383,9 +383,7 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const
   }
   else if(type.id()==ID_vector)
     return is_complete_type(type.subtype());
-  else if(
-    type.id() == ID_symbol_type || type.id() == ID_struct_tag ||
-    type.id() == ID_union_tag)
+  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
   {
     return is_complete_type(follow(type));
   }
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 384375b2409..9ec19b35d95 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -91,11 +91,6 @@ bool c_typecheck_baset::gcc_types_compatible_p(
   // read
   // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
 
-  if(type1.id() == ID_symbol_type)
-    return gcc_types_compatible_p(follow(type1), type2);
-  else if(type2.id() == ID_symbol_type)
-    return gcc_types_compatible_p(type1, follow(type2));
-
   // check qualifiers first
   if(c_qualifierst(type1)!=c_qualifierst(type2))
     return false;
@@ -3158,9 +3153,6 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
 
   typet subtype=type.subtype();
 
-  if(subtype.id() == ID_symbol_type)
-    subtype = follow(to_symbol_type(subtype));
-
   if(subtype.id()==ID_incomplete_struct)
   {
     err_location(expr);
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 0ecd67a19ad..2bb1dc370d1 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -89,8 +89,6 @@ void c_typecheck_baset::typecheck_type(typet &type)
     typecheck_c_bit_field_type(to_c_bit_field_type(type));
   else if(type.id()==ID_typeof)
     typecheck_typeof_type(type);
-  else if(type.id() == ID_symbol_type)
-    typecheck_symbol_type(to_symbol_type(type));
   else if(type.id() == ID_typedef_type)
     typecheck_typedef_type(type);
   else if(type.id() == ID_struct_tag ||
@@ -1458,32 +1456,6 @@ void c_typecheck_baset::typecheck_typeof_type(typet &type)
   c_qualifiers.write(type);
 }
 
-void c_typecheck_baset::typecheck_symbol_type(symbol_typet &type)
-{
-  // we do some consistency checking only
-  const irep_idt &identifier = type.get_identifier();
-
-  symbol_tablet::symbolst::const_iterator s_it=
-    symbol_table.symbols.find(identifier);
-
-  if(s_it==symbol_table.symbols.end())
-  {
-    error().source_location=type.source_location();
-    error() << "type symbol `" << identifier << "' not found"
-            << eom;
-    throw 0;
-  }
-
-  const symbolt &symbol=s_it->second;
-
-  if(!symbol.is_type)
-  {
-    error().source_location=type.source_location();
-    error() << "expected type symbol" << eom;
-    throw 0;
-  }
-}
-
 void c_typecheck_baset::typecheck_typedef_type(typet &type)
 {
   const irep_idt &identifier = to_typedef_type(type).get_identifier();
diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index ba4771f97ba..e024fa4b6f9 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -86,8 +86,6 @@ mp_integer alignment(const typet &type, const namespacet &ns)
     result = alignment(ns.follow_tag(to_struct_tag_type(type)), ns);
   else if(type.id() == ID_union_tag)
     result = alignment(ns.follow_tag(to_union_tag_type(type)), ns);
-  else if(type.id() == ID_symbol_type)
-    result = alignment(ns.follow(to_symbol_type(type)), ns);
   else if(type.id()==ID_c_bit_field)
   {
     // we align these according to the 'underlying type'