--- 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);