Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more careful declaration of "inducts";
authorwenzelm
Thu, 23 Nov 2006 23:05:28 +0100
changeset 21508 3029fb2d5650
parent 21507 f67b41110edd
child 21509 6c5755ad9cae
more careful declaration of "inducts";
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle