# HG changeset patch
# User krauss
# Date 1312283220 -7200
# Node ID e828be67dfe75794bddc1cb3320fbff0e6224d00
# Parent  51184010c60953e121d4d5b795ef7b7489e16ec2
updated unchecked forward reference

diff -r 51184010c609 -r e828be67dfe7 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