src/HOL/Tools/inductive_package.ML
changeset 8380 c96953faf0a4
parent 8375 0544749a5e8f
child 8401 50d5f4402305
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 08 23:43:11 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 08 23:45:37 2000 +0100
     1.3 @@ -276,12 +276,6 @@
     1.4  
     1.5  (** elimination rules **)
     1.6  
     1.7 -fun tune_names raw_names =
     1.8 -  let
     1.9 -    fun tune ("", i) = Library.string_of_int i
    1.10 -      | tune (s, _) = s;
    1.11 -  in map2 tune (raw_names, 0 upto (length raw_names - 1)) end;
    1.12 -
    1.13  fun mk_elims cs cTs params intr_ts intr_names =
    1.14    let
    1.15      val used = foldr add_term_names (intr_ts, []);
    1.16 @@ -293,7 +287,7 @@
    1.17          HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
    1.18        in (u, t, Logic.strip_imp_prems r) end;
    1.19  
    1.20 -    val intrs = map dest_intr intr_ts ~~ tune_names intr_names;
    1.21 +    val intrs = map dest_intr intr_ts ~~ intr_names;
    1.22  
    1.23      fun mk_elim (c, T) =
    1.24        let
    1.25 @@ -407,8 +401,7 @@
    1.26      val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
    1.27  
    1.28      fun induct_spec (name, th) =
    1.29 -      (("", th), [RuleCases.case_names (tune_names induct_cases),
    1.30 -        InductMethod.induct_set_global name]);
    1.31 +      (("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name]);
    1.32      val induct_specs =
    1.33        if no_ind then []
    1.34        else map induct_spec (project_rules names induct);