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/Nitpick/nitpick_hol.ML
changeset 55017 2df6ad1dbd66
parent 54816 10d48c2a3e32
child 55080 b7c41accbff2 
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jan 16 15:47:33 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jan 16 16:20:17 2014 +0100
@@ -1832,7 +1832,7 @@
                                    "too many nested definitions (" ^
                                    string_of_int depth ^ ") while expanding " ^
                                    quote s)
-                else if s = "Wfrec.wfrec'" (* FIXME unchecked! *) then
+                else if s = @{const_name wfrec'} then
                   (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
                 else if not unfold andalso
                      size_of_term def > def_inline_threshold () then
isabelle