diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
index 859b99a2d36..641c05a13ed 100644
--- a/src/ansi-c/ansi_c_declaration.cpp
+++ b/src/ansi-c/ansi_c_declaration.cpp
@@ -22,12 +22,12 @@ void ansi_c_declaratort::build(irept &src)
 {
   typet *p=static_cast<typet *>(&src);
 
-  // walk down subtype until we hit symbol or "abstract"
+  // walk down subtype until we hit typedef_type, symbol or "abstract"
   while(true)
   {
     typet &t=*p;
 
-    if(t.id()==ID_symbol)
+    if(t.id() == ID_typedef_type || t.id() == ID_symbol)
     {
       set_base_name(t.get(ID_C_base_name));
       add_source_location()=t.source_location();
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 197251fad21..172ac693a40 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/src/ansi-c/c_typecheck_base.h
@@ -209,7 +209,8 @@ 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(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);
   virtual void typecheck_array_type(array_typet &type);
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index edcef9e5c80..c6767fb40e1 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "gcc_types.h"
 #include "padding.h"
 #include "type2name.h"
+#include "typedef_type.h"
 
 void c_typecheck_baset::typecheck_type(typet &type)
 {
@@ -89,7 +90,9 @@ void c_typecheck_baset::typecheck_type(typet &type)
   else if(type.id()==ID_typeof)
     typecheck_typeof_type(type);
   else if(type.id()==ID_symbol)
-    typecheck_symbol_type(type);
+    typecheck_symbol_type(to_symbol_type(type));
+  else if(type.id() == ID_typedef_type)
+    typecheck_typedef_type(type);
   else if(type.id()==ID_vector)
     typecheck_vector_type(to_vector_type(type));
   else if(type.id()==ID_custom_unsignedbv ||
@@ -1425,10 +1428,10 @@ void c_typecheck_baset::typecheck_typeof_type(typet &type)
   c_qualifiers.write(type);
 }
 
-void c_typecheck_baset::typecheck_symbol_type(typet &type)
+void c_typecheck_baset::typecheck_symbol_type(symbol_typet &type)
 {
-  const irep_idt &identifier=
-    to_symbol_type(type).get_identifier();
+  // 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);
@@ -1449,25 +1452,46 @@ void c_typecheck_baset::typecheck_symbol_type(typet &type)
     error() << "expected type symbol" << eom;
     throw 0;
   }
+}
 
-  if(symbol.is_macro)
-  {
-    // overwrite, but preserve (add) any qualifiers and other flags
+void c_typecheck_baset::typecheck_typedef_type(typet &type)
+{
+  const irep_idt &identifier = to_typedef_type(type).get_identifier();
 
-    c_qualifierst c_qualifiers(type);
-    bool is_packed=type.get_bool(ID_C_packed);
-    irept alignment=type.find(ID_C_alignment);
+  symbol_tablet::symbolst::const_iterator s_it =
+    symbol_table.symbols.find(identifier);
 
-    c_qualifiers+=c_qualifierst(symbol.type);
-    type=symbol.type;
-    c_qualifiers.write(type);
+  if(s_it == symbol_table.symbols.end())
+  {
+    error().source_location = type.source_location();
+    error() << "typedef symbol `" << identifier << "' not found" << eom;
+    throw 0;
+  }
 
-    if(is_packed)
-      type.set(ID_C_packed, true);
-    if(alignment.is_not_nil())
-      type.set(ID_C_alignment, alignment);
+  const symbolt &symbol = s_it->second;
+
+  if(!symbol.is_type)
+  {
+    error().source_location = type.source_location();
+    error() << "expected type symbol for typedef" << eom;
+    throw 0;
   }
 
+  // overwrite, but preserve (add) any qualifiers and other flags
+
+  c_qualifierst c_qualifiers(type);
+  bool is_packed = type.get_bool(ID_C_packed);
+  irept alignment = type.find(ID_C_alignment);
+
+  c_qualifiers += c_qualifierst(symbol.type);
+  type = symbol.type;
+  c_qualifiers.write(type);
+
+  if(is_packed)
+    type.set(ID_C_packed, true);
+  if(alignment.is_not_nil())
+    type.set(ID_C_alignment, alignment);
+
   // CPROVER extensions
   if(symbol.base_name=="__CPROVER_rational")
   {
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
index 965d14a14c1..09125b12da8 100644
--- a/src/ansi-c/scanner.l
+++ b/src/ansi-c/scanner.l
@@ -92,15 +92,20 @@ int make_identifier()
 
     PARSER.tag_following=false;
 
-    stack(yyansi_clval).id(ID_symbol);
     stack(yyansi_clval).set(ID_C_base_name, base_name);
     stack(yyansi_clval).set(ID_identifier, identifier);
     stack(yyansi_clval).set(ID_C_id_class, static_cast<int>(result));
 
     if(result==ansi_c_id_classt::ANSI_C_TYPEDEF)
+    {
+      stack(yyansi_clval).id(ID_typedef_type);
       return TOK_TYPEDEFNAME;
+    }
     else
+    {
+      stack(yyansi_clval).id(ID_symbol);
       return TOK_IDENTIFIER;
+    }
   }
 }
 
diff --git a/src/ansi-c/typedef_type.h b/src/ansi-c/typedef_type.h
new file mode 100644
index 00000000000..cc76befbc56
--- /dev/null
+++ b/src/ansi-c/typedef_type.h
@@ -0,0 +1,66 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_ANSI_C_TYPEDEF_TYPE_H
+#define CPROVER_ANSI_C_TYPEDEF_TYPE_H
+
+#include <util/type.h>
+
+/*! \brief A typedef
+*/
+class typedef_typet : public typet
+{
+public:
+  explicit typedef_typet(const irep_idt &identifier) : typet(ID_typedef_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);
+  }
+};
+
+/*! \brief Cast a generic typet to a \ref typedef_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * typedef_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref typedef_typet
+ *
+ * \ingroup gr_std_types
+*/
+inline const typedef_typet &to_typedef_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_typedef_type);
+  return static_cast<const typedef_typet &>(type);
+}
+
+/*! \copydoc to_typedef_type(const typet &)
+ * \ingroup gr_std_types
+*/
+inline typedef_typet &to_typedef_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_typedef_type);
+  return static_cast<typedef_typet &>(type);
+}
+
+template <>
+inline bool can_cast_type<typedef_typet>(const typet &type)
+{
+  return type.id() == ID_typedef_type;
+}
+
+#endif // CPROVER_ANSI_C_TYPEDEF_TYPE_H
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 151eb6f6b6e..baa9fb3dcd7 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -244,6 +244,7 @@ IREP_ID_ONE(concatenation)
 IREP_ID_ONE(infinity)
 IREP_ID_ONE(return_type)
 IREP_ID_ONE(typedef)
+IREP_ID_ONE(typedef_type)
 IREP_ID_TWO(C_typedef, #typedef)
 IREP_ID_ONE(extern)
 IREP_ID_ONE(static)