# HG changeset patch
# User wenzelm
# Date 1164319528 -3600
# Node ID 3029fb2d56507be56bdf91c1f1cb30cc4deb26ef
# Parent  f67b41110edd2a860c4ef2d0ba748a2a5ba296a6
more careful declaration of "inducts";

diff -r f67b41110edd -r 3029fb2d5650 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Nov 23 22:38:32 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Nov 23 23:05:28 2006 +0100
@@ -684,13 +684,11 @@
       let val inducts = cnames ~~ ProjectRule.projects ctxt (1 upto length cnames) induct'
       in
         ctxt3 |>
-        note_theorems (inducts |> map (fn (name, th) => (("",
-          [Attrib.internal ind_case_names,
-           Attrib.internal (RuleCases.consumes 1),
-           Attrib.internal (induct_att name)]), [([th], [])]))) |> snd |>
-        note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"),
-          [Attrib.internal ind_case_names,
-           Attrib.internal (RuleCases.consumes 1)]), map snd inducts) |> snd
+        note_theorems [((NameSpace.qualified rec_name (coind_prefix coind ^ "inducts"), []),
+          inducts |> map (fn (name, th) => ([th],
+            [Attrib.internal ind_case_names,
+             Attrib.internal (RuleCases.consumes 1),
+             Attrib.internal (induct_att name)])))] |> snd
       end;
 
     val result =