tuned;
authorwenzelm
Tue Nov 13 22:18:46 2001 +0100 (2001-11-13 ago)
changeset 121725e81c9d539f8
parent 12171 dc87f33db447
child 12173 f3f7993ae6da
tuned;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Nov 13 22:18:03 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Nov 13 22:18:46 2001 +0100
     1.3 @@ -455,7 +455,7 @@
     1.4              RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
     1.5        in names ~~ map proj (1 upto n) end;
     1.6  
     1.7 -fun add_cases_induct no_elim no_ind names elims induct =
     1.8 +fun add_cases_induct no_elim no_induct names elims induct =
     1.9    let
    1.10      fun cases_spec (name, elim) thy =
    1.11        thy
    1.12 @@ -466,7 +466,7 @@
    1.13  
    1.14      fun induct_spec (name, th) = #1 o PureThy.add_thms
    1.15        [(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])];
    1.16 -    val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
    1.17 +    val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct);
    1.18    in Library.apply (cases_specs @ induct_specs) end;
    1.19  
    1.20  
    1.21 @@ -586,8 +586,7 @@
    1.22  
    1.23  (* inductive_cases(_i) *)
    1.24  
    1.25 -fun gen_inductive_cases prep_att prep_const prep_prop
    1.26 -    (((name, raw_atts), raw_props), comment) thy =
    1.27 +fun gen_inductive_cases prep_att prep_prop (((name, raw_atts), raw_props), comment) thy =
    1.28    let
    1.29      val ss = Simplifier.simpset_of thy;
    1.30      val sign = Theory.sign_of thy;
    1.31 @@ -599,10 +598,8 @@
    1.32      IsarThy.have_theorems_i Drule.lemmaK [(((name, atts), map Thm.no_attributes thms), comment)]
    1.33    end;
    1.34  
    1.35 -val inductive_cases =
    1.36 -  gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
    1.37 -
    1.38 -val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
    1.39 +val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
    1.40 +val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
    1.41  
    1.42  
    1.43  (* mk_cases_meth *)
    1.44 @@ -843,7 +840,8 @@
    1.45          con_defs thy params paramTs cTs cnames induct_cases;
    1.46      val thy2 = thy1
    1.47        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    1.48 -      |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct;
    1.49 +      |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
    1.50 +          full_cnames elims induct;
    1.51    in (thy2, result) end;
    1.52  
    1.53  fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =