src/HOL/Tools/Datatype/datatype_aux.ML
changeset 32727 9072201cd69d
parent 32718 45929374f1bd
child 32733 71618deaf777
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 09:47:32 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 10:20:21 2009 +0200
     1.3 @@ -193,7 +193,8 @@
     1.4     sorts : (string * sort) list,
     1.5     inject : thm list,
     1.6     distinct : simproc_dist,
     1.7 -   inducts : thm list * thm,
     1.8 +   induct : thm,
     1.9 +   inducts : thm list,
    1.10     exhaust : thm,
    1.11     nchotomy : thm,
    1.12     rec_names : string list,
    1.13 @@ -202,7 +203,8 @@
    1.14     case_rewrites : thm list,
    1.15     case_cong : thm,
    1.16     weak_case_cong : thm,
    1.17 -   splits : thm * thm};
    1.18 +   split : thm,
    1.19 +   split_asm: thm};
    1.20  
    1.21  fun mk_Free s T i = Free (s ^ (string_of_int i), T);
    1.22