updated unchecked forward reference
authorkrauss
Tue Aug 02 13:07:00 2011 +0200 (2011-08-02)
changeset 44017e828be67dfe7
parent 44016 51184010c609
child 44018 d34f0cd62164
updated unchecked forward reference
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 12:27:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 13:07:00 2011 +0200
     1.3 @@ -1779,7 +1779,7 @@
     1.4                                     "too many nested definitions (" ^
     1.5                                     string_of_int depth ^ ") while expanding " ^
     1.6                                     quote s)
     1.7 -                else if s = "Old_Recdef.wfrec'" (* FIXME unchecked! *) then
     1.8 +                else if s = "Wfrec.wfrec'" (* FIXME unchecked! *) 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