added the_mk_cases;

--- a/src/HOL/Tools/inductive_package.ML	Thu Dec 06 00:40:19 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 06 00:40:56 2001 +0100
@@ -36,6 +36,7 @@
   val get_inductive: theory -> string -> ({names: string list, coind: bool} *
     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
+  val the_mk_cases: theory -> string -> string -> thm
   val print_inductives: theory -> unit
   val mono_add_global: theory attribute
   val mono_del_global: theory attribute
@@ -120,6 +121,8 @@
     None => error ("Unknown (co)inductive set " ^ quote name)
   | Some info => info);
 
+val the_mk_cases = (#mk_cases o #2) oo the_inductive;
+
 fun put_inductives names info thy =
   let
     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);