# HG changeset patch
# User wenzelm
# Date 1011049731 -3600
# Node ID a906a8b364f111549ee3aef6a3e12e524830f800
# Parent  044a59921f3ba5416bf3fcfde54a238e45a854d3
removed case_numbers (already covered by default);

diff -r 044a59921f3b -r a906a8b364f1 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Jan 15 00:08:11 2002 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Tue Jan 15 00:08:51 2002 +0100
@@ -245,12 +245,11 @@
     val simp_att = if null tcs then
       [Simplifier.simp_add_global, RecfunCodegen.add] else [];
 
-    val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
     val (thy, (simps' :: rules', [induct'])) =
       thy
       |> Theory.add_path bname
       |> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
-      |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
+      |>>> PureThy.add_thms [(("induct", induct), [])];
     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy =
       thy