# HG changeset patch
# User wenzelm
# Date 1007595656 -3600
# Node ID f12f95e216e05fb13475704ea1f64d17e62a9cff
# Parent  2ba27248af7f89934fae60a18ab3d65c05ba9eb3
added the_mk_cases;

diff -r 2ba27248af7f -r f12f95e216e0 src/HOL/Tools/inductive_package.ML
--- 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);