removed case_numbers (already covered by default);
authorwenzelm
Tue, 15 Jan 2002 00:08:51 +0100
changeset 12755 a906a8b364f1
parent 12754 044a59921f3b
child 12756 08bf3d911968
removed case_numbers (already covered by default);
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