changeset 41792 | ff3cb0c418b7 |
parent 41228 | e1fce873b814 |
child 42358 | b47d41d9f4b5 |
--- 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;