TODO: handle internal / external names;

--- a/src/HOL/datatype.ML	Mon Oct 06 19:11:56 1997 +0200
+++ b/src/HOL/datatype.ML	Mon Oct 06 19:13:29 1997 +0200
@@ -3,6 +3,9 @@
    Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker,
                 Konrad Slind
    Copyright 1995 TU Muenchen
+
+TODO:
+  - handle internal / external names
 *)
 
 (** Information about datatypes **)