updated unchecked forward reference
authorkrauss
Tue, 02 Aug 2011 13:07:00 +0200
changeset 44017 e828be67dfe7
parent 44016 51184010c609
child 44018 d34f0cd62164
updated unchecked forward reference
src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 12:27:24 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 13:07:00 2011 +0200
@@ -1779,7 +1779,7 @@
                                    "too many nested definitions (" ^
                                    string_of_int depth ^ ") while expanding " ^
                                    quote s)
-                else if s = "Old_Recdef.wfrec'" (* FIXME unchecked! *) then
+                else if s = "Wfrec.wfrec'" (* FIXME unchecked! *) then
                   (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
                 else if not unfold andalso
                      size_of_term def > def_inline_threshold () then