diff -r 01d722707a36 -r ff3cb0c418b7 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Feb 21 10:42:29 2011 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Feb 21 10:44:19 2011 +0100
@@ -774,7 +774,7 @@
       |> Local_Theory.conceal
       |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
+         ((Binding.empty, [Attrib.internal (K Nitpick_Unfolds.add)]),
          fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
       ||> Local_Theory.restore_naming lthy;