# HG changeset patch
# User blanchet
# Date 1257418687 -3600
# Node ID ea36b70a6c1cbc4d31af5b157c9bcaab0578a897
# Parent  82ba4d566192cf21615a179fbd3730ffed17a6d5
added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package;
this ensures that Nitpick can find the definition and determine whether its inductive
or coinductive

diff -r 82ba4d566192 -r ea36b70a6c1c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Oct 29 23:08:51 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Thu Nov 05 11:58:07 2009 +0100
@@ -653,7 +653,8 @@
       |> LocalTheory.conceal
       |> LocalTheory.define Thm.internalK
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         (Attrib.empty_binding, fold_rev lambda params
+         ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
+         fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
       ||> LocalTheory.restore_naming ctxt;
     val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])