--- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Nov 30 21:14:01 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Nov 30 23:30:08 2011 +0100
@@ -15,7 +15,6 @@
type descr = (int * (string * dtyp list * (string * dtyp list) list)) list
type info =
{index : int,
- alt_names : string list option,
descr : descr,
sorts : (string * sort) list,
inject : thm list,
@@ -188,7 +187,6 @@
type info =
{index : int,
- alt_names : string list option,
descr : descr,
sorts : (string * sort) list,
inject : thm list,