Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_package.ML
changeset 29863 dadad1831e9d
parent 29581 b3b33e0298eb
child 29866 6e93ae65c678 
--- a/src/HOL/Tools/inductive_package.ML	Fri Feb 06 13:43:19 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Feb 06 15:57:47 2009 +0100
@@ -691,7 +691,8 @@
       ctxt |>
       LocalTheory.notes kind
         (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
-           [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
+           [Attrib.internal (K (ContextRules.intro_query NONE)),
+            Attrib.internal (K Nitpick_Ind_Intros_Thms.add)])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
       ctxt1 |>
isabelle