src/HOL/Tools/ATP/atp_problem.ML

--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu May 12 15:29:19 2011 +0200
@@ -171,6 +171,7 @@
       | keep (c :: cs) = c :: keep cs
   in String.explode #> rev #> keep #> rev #> String.implode end
 
+(* Long names can slow down the ATPs. *)
 val max_readable_name_size = 20
 
 (* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the