src/HOL/simpdata.ML

--- a/src/HOL/simpdata.ML	Wed May 21 17:31:12 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu May 22 09:20:28 1997 +0200
@@ -351,7 +351,9 @@
                    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;