src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 44013 5cfc1c36ae97
parent 44012 8c1dfd6c2262
child 44016 51184010c609
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 10:03:14 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 10:36:50 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 = @{const_name wfrec'} then
     1.8 +                else if s = "Old_Recdef.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
    1.12 @@ -1873,9 +1873,7 @@
    1.13    [(@{const_name card}, @{const_name card'}),
    1.14     (@{const_name setsum}, @{const_name setsum'}),
    1.15     (@{const_name fold_graph}, @{const_name fold_graph'}),
    1.16 -   (@{const_name wf}, @{const_name wf'}),
    1.17 -   (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    1.18 -   (@{const_name wfrec}, @{const_name wfrec'})]
    1.19 +   (@{const_name wf}, @{const_name wf'})]
    1.20  
    1.21  fun ersatz_table ctxt =
    1.22   (basic_ersatz_table @ #ersatz_table (Data.get (Context.Proof ctxt)))