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