added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package;
authorblanchet
Thu, 05 Nov 2009 11:58:07 +0100
changeset 33577 ea36b70a6c1c
parent 33576 82ba4d566192
child 33578 0c3ba1e010d2
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
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])