1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Dec 29 18:34:42 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Dec 29 18:35:27 2001 +0100
     1.3 @@ -44,9 +44,9 @@
     1.4    val inductive_forall_name: string
     1.5    val inductive_forall_def: thm
     1.6    val rulify: thm -> thm
     1.7 -  val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
     1.8 +  val inductive_cases: (((bstring * Args.src list) * string list) * Comment.text) list
     1.9      -> theory -> theory
    1.10 -  val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    1.11 +  val inductive_cases_i: (((bstring * theory attribute list) * term list) * Comment.text) list
    1.12      -> theory -> theory
    1.13    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    1.14      ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    1.15 @@ -582,17 +582,14 @@
    1.16  
    1.17  (* inductive_cases(_i) *)
    1.18  
    1.19 -fun gen_inductive_cases prep_att prep_prop (((name, raw_atts), raw_props), comment) thy =
    1.20 +fun gen_inductive_cases prep_att prep_prop args thy =
    1.21    let
    1.22 -    val ss = Simplifier.simpset_of thy;
    1.23 -    val sign = Theory.sign_of thy;
    1.24 -    val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
    1.25 -    val atts = map (prep_att thy) raw_atts;
    1.26 -    val thms = map (smart_mk_cases thy ss) cprops;
    1.27 -  in
    1.28 -    thy |>
    1.29 -    IsarThy.have_theorems_i Drule.lemmaK [(((name, atts), map Thm.no_attributes thms), comment)]
    1.30 -  end;
    1.31 +    val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
    1.32 +    val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
    1.33 +
    1.34 +    val facts = args |> map (fn (((name, atts), props), comment) =>
    1.35 +      (((name, map (prep_att thy) atts), map (Thm.no_attributes o mk_cases) props), comment));
    1.36 +  in thy |> IsarThy.have_theorems_i Drule.lemmaK facts end;
    1.37  
    1.38  val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
    1.39  val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
    1.40 @@ -891,7 +888,7 @@
    1.41  
    1.42  
    1.43  val ind_cases =
    1.44 -  P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
    1.45 +  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment)
    1.46    >> (Toplevel.theory o inductive_cases);
    1.47  
    1.48  val inductive_casesP =

     2.1 --- a/src/ZF/Tools/ind_cases.ML	Sat Dec 29 18:34:42 2001 +0100
     2.2 +++ b/src/ZF/Tools/ind_cases.ML	Sat Dec 29 18:35:27 2001 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  signature IND_CASES =
     2.5  sig
     2.6    val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
     2.7 -  val inductive_cases: ((bstring * Args.src list) * string list) -> theory -> theory
     2.8 +  val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
     2.9    val setup: (theory -> theory) list
    2.10  end;
    2.11  
    2.12 @@ -50,15 +50,14 @@
    2.13  
    2.14  (* inductive_cases command *)
    2.15  
    2.16 -fun inductive_cases ((name, srcs), props) thy =
    2.17 +fun inductive_cases args thy =
    2.18    let
    2.19      val read_prop = ProofContext.read_prop (ProofContext.init thy);
    2.20 -    val ths = map (smart_cases thy (Simplifier.simpset_of thy) read_prop) props;
    2.21 -    val atts = map (Attrib.global_attribute thy) srcs;
    2.22 -  in
    2.23 -    thy |> IsarThy.have_theorems_i Drule.lemmaK
    2.24 -      [(((name, atts), map Thm.no_attributes ths), Comment.none)]
    2.25 -  end;
    2.26 +    val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
    2.27 +    val facts = args |> map (fn ((name, srcs), props) =>
    2.28 +      (((name, map (Attrib.global_attribute thy) srcs), map (Thm.no_attributes o mk_cases) props),
    2.29 +        Comment.none));
    2.30 +  in thy |> IsarThy.have_theorems_i Drule.lemmaK facts end;
    2.31  
    2.32  
    2.33  (* ind_cases method *)
    2.34 @@ -85,7 +84,7 @@
    2.35  local structure P = OuterParse and K = OuterSyntax.Keyword in
    2.36  
    2.37  val ind_cases =
    2.38 -  P.opt_thm_name ":" -- Scan.repeat1 P.prop --| P.marg_comment
    2.39 +  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop --| P.marg_comment)
    2.40    >> (Toplevel.theory o inductive_cases);
    2.41  
    2.42  val inductive_casesP =