Deleted obsolete comments.

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 30 15:52:33 1998 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 30 15:54:03 1998 +0200
@@ -41,14 +41,6 @@
 
 (******************************************************************************)
 
-(*----------------------------------------------------------*)
-(* Proofs dependent on concrete representation of datatypes *)
-(*                                                          *)
-(* - injectivity of constructors                            *)
-(* - distinctness of constructors (internal version)        *)
-(* - induction theorem                                      *)
-(*----------------------------------------------------------*)
-
 fun representation_proofs (dt_info : datatype_info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax thy =
   let