diff --git a/src/util/std_types.h b/src/util/std_types.h
index 9693f10b78e..792f7e40ab8 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -974,6 +974,12 @@ class code_typet:public typet
   }
 };
 
+template <>
+inline bool can_cast_type<code_typet>(const typet &type)
+{
+  return type.id() == ID_code;
+}
+
 /*! \brief Cast a generic typet to a \ref code_typet
  *
  * This is an unchecked conversion. \a type must be known to be \ref
@@ -986,7 +992,8 @@ class code_typet:public typet
 */
 inline const code_typet &to_code_type(const typet &type)
 {
-  PRECONDITION(type.id()==ID_code);
+  PRECONDITION(can_cast_type<code_typet>(type));
+  validate_type(type);
   return static_cast<const code_typet &>(type);
 }
 
@@ -995,10 +1002,12 @@ inline const code_typet &to_code_type(const typet &type)
 */
 inline code_typet &to_code_type(typet &type)
 {
-  PRECONDITION(type.id()==ID_code);
+  PRECONDITION(can_cast_type<code_typet>(type));
+  validate_type(type);
   return static_cast<code_typet &>(type);
 }
 
+
 /*! \brief arrays with given size
 */
 class array_typet:public type_with_subtypet