Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive.ML
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;
isabelle