improve optimization
authorblanchet
Mon, 21 Feb 2011 11:50:38 +0100
changeset 4266679a79460b70c
parent 42665 03bf23a265b6
child 42667 afd7405f1d7e
improve optimization
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 11:50:37 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 11:50:38 2011 +0100
     1.3 @@ -343,9 +343,7 @@
     1.4  
     1.5  fun s_let Ts s n abs_T body_T f t =
     1.6    if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
     1.7 -     is_special_eligible_arg true Ts t then
     1.8 -     (* TODO: the "true" argument to "is_special_eligible_arg" should perhaps be
     1.9 -        "false" instead to account for potential future specializations. *)
    1.10 +     is_special_eligible_arg false Ts t then
    1.11      f t
    1.12    else
    1.13      let val z = (let_var s, abs_T) in