# 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 =