src/HOL/Tools/Datatype/datatype_aux.ML
changeset 32964 2d7e1ab55037
parent 32952 aeb1e44fbc19
child 33037 b22e44496dc2
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Oct 17 14:51:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Oct 17 15:42:36 2009 +0200
     1.3 @@ -6,14 +6,32 @@
     1.4  
     1.5  signature DATATYPE_COMMON =
     1.6  sig
     1.7 -  type config
     1.8 +  type config = {strict : bool, quiet : bool}
     1.9    val default_config : config
    1.10    datatype dtyp =
    1.11        DtTFree of string
    1.12 -    | DtType of string * (dtyp list)
    1.13 -    | DtRec of int;
    1.14 -  type descr
    1.15 -  type info
    1.16 +    | DtType of string * dtyp list
    1.17 +    | DtRec of int
    1.18 +  type descr = (int * (string * dtyp list * (string * dtyp list) list)) list
    1.19 +  type info =
    1.20 +   {index : int,
    1.21 +    alt_names : string list option,
    1.22 +    descr : descr,
    1.23 +    sorts : (string * sort) list,
    1.24 +    inject : thm list,
    1.25 +    distinct : thm list,
    1.26 +    induct : thm,
    1.27 +    inducts : thm list,
    1.28 +    exhaust : thm,
    1.29 +    nchotomy : thm,
    1.30 +    rec_names : string list,
    1.31 +    rec_rewrites : thm list,
    1.32 +    case_name : string,
    1.33 +    case_rewrites : thm list,
    1.34 +    case_cong : thm,
    1.35 +    weak_case_cong : thm,
    1.36 +    split : thm,
    1.37 +    split_asm: thm}
    1.38  end
    1.39  
    1.40  signature DATATYPE_AUX =
    1.41 @@ -68,11 +86,11 @@
    1.42  
    1.43  (* datatype option flags *)
    1.44  
    1.45 -type config = { strict: bool, quiet: bool };
    1.46 -val default_config : config =
    1.47 -  { strict = true, quiet = false };
    1.48 -fun message ({ quiet, ...} : config) s =
    1.49 -  if quiet then () else writeln s;
    1.50 +type config = {strict : bool, quiet : bool};
    1.51 +val default_config : config = {strict = true, quiet = false};
    1.52 +
    1.53 +fun message ({quiet = true, ...} : config) s = writeln s
    1.54 +  | message _ _ = ();
    1.55  
    1.56  
    1.57  (* store theorems in theory *)