# HG changeset patch
# User wenzelm
# Date 952555537 -3600
# Node ID c96953faf0a4ba3ffab789e31c7d9ea52bb3ce8d
# Parent  4c7659e98eb97610d97cece2def31f17919d5c3c
removed tune_names;

diff -r 4c7659e98eb9 -r c96953faf0a4 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Mar 08 23:43:11 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 08 23:45:37 2000 +0100
@@ -276,12 +276,6 @@
 
 (** elimination rules **)
 
-fun tune_names raw_names =
-  let
-    fun tune ("", i) = Library.string_of_int i
-      | tune (s, _) = s;
-  in map2 tune (raw_names, 0 upto (length raw_names - 1)) end;
-
 fun mk_elims cs cTs params intr_ts intr_names =
   let
     val used = foldr add_term_names (intr_ts, []);
@@ -293,7 +287,7 @@
         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
       in (u, t, Logic.strip_imp_prems r) end;
 
-    val intrs = map dest_intr intr_ts ~~ tune_names intr_names;
+    val intrs = map dest_intr intr_ts ~~ intr_names;
 
     fun mk_elim (c, T) =
       let
@@ -407,8 +401,7 @@
     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
 
     fun induct_spec (name, th) =
-      (("", th), [RuleCases.case_names (tune_names induct_cases),
-        InductMethod.induct_set_global name]);
+      (("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name]);
     val induct_specs =
       if no_ind then []
       else map induct_spec (project_rules names induct);