# HG changeset patch
# User blanchet
# Date 1298285438 -3600
# Node ID 79a79460b70cf160822c743b579256f725588cd6
# Parent  03bf23a265b683ae978898747601addb71090faa
improve optimization

diff -r 03bf23a265b6 -r 79a79460b70c src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 11:50:37 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 11:50:38 2011 +0100
@@ -343,9 +343,7 @@
 
 fun s_let Ts s n abs_T body_T f t =
   if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
-     is_special_eligible_arg true Ts t then
-     (* TODO: the "true" argument to "is_special_eligible_arg" should perhaps be
-        "false" instead to account for potential future specializations. *)
+     is_special_eligible_arg false Ts t then
     f t
   else
     let val z = (let_var s, abs_T) in