src/HOL/Tools/inductive_package.ML
changeset 12400 f12f95e216e0
parent 12338 de0f4a63baa5
child 12494 58848edad3c4
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 06 00:40:19 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 06 00:40:56 2001 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4    val get_inductive: theory -> string -> ({names: string list, coind: bool} *
     1.5      {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
     1.6       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
     1.7 +  val the_mk_cases: theory -> string -> string -> thm
     1.8    val print_inductives: theory -> unit
     1.9    val mono_add_global: theory attribute
    1.10    val mono_del_global: theory attribute
    1.11 @@ -120,6 +121,8 @@
    1.12      None => error ("Unknown (co)inductive set " ^ quote name)
    1.13    | Some info => info);
    1.14  
    1.15 +val the_mk_cases = (#mk_cases o #2) oo the_inductive;
    1.16 +
    1.17  fun put_inductives names info thy =
    1.18    let
    1.19      fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);