src/HOL/simpdata.ML

 
 type dtype_info = {case_const:term,
                    case_rewrites:thm list,
                    constructors:term list,
                    induct_tac: string -> int -> tactic,
-                   nchotomy:thm,
+                   nchotomy: thm,
+                   exhaustion: thm,
+                   exhaust_tac: string -> int -> tactic,
                    case_cong:thm};
 
 exception DT_DATA of (string * dtype_info) list;
 val datatypes = ref [] : (string * dtype_info) list ref;