1.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Mar 20 17:04:44 2009 +0100
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Mar 20 17:12:37 2009 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4      dom_subset : thm,                  (*inclusion of recursive set in dom*)
     1.5      intrs      : thm list,             (*introduction rules*)
     1.6      elim       : thm,                  (*case analysis theorem*)
     1.7 -    mk_cases   : string -> thm,        (*generates case theorems*)
     1.8      induct     : thm,                  (*main induction rule*)
     1.9      mutual_induct : thm};              (*mutual induction rule*)
    1.10  
    1.11 @@ -275,9 +274,6 @@
    1.12        (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac)
    1.13        (Thm.assume A RS elim)
    1.14        |> Drule.standard';
    1.15 -  fun mk_cases a = make_cases (*delayed evaluation of body!*)
    1.16 -    (simpset ())
    1.17 -    let val thy = Thm.theory_of_thm elim in cterm_of thy (Syntax.read_prop_global thy a) end;
    1.18  
    1.19    fun induction_rules raw_induct thy =
    1.20     let
    1.21 @@ -548,7 +544,6 @@
    1.22         dom_subset = dom_subset',
    1.23         intrs = intrs'',
    1.24         elim = elim',
    1.25 -       mk_cases = mk_cases,
    1.26         induct = induct,
    1.27         mutual_induct = mutual_induct})
    1.28    end;