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