# HG changeset patch
# User blanchet
# Date 1314713265 -7200
# Node ID 54906b0337ab99b75bc44528e9efe1963948057b
# Parent  0b107d11f6344292d6bd7254833ea753f5af42db
flip logic of boolean option so it's off by default

diff -r 0b107d11f634 -r 54906b0337ab src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:07:45 2011 +0200
@@ -64,7 +64,7 @@
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
   val atp_lambda_translation : string Config.T
-  val atp_readable_names : bool Config.T
+  val atp_full_names : bool Config.T
   val atp_sound_modulo_infiniteness : bool Config.T
   val smt_triggers : bool Config.T
   val smt_weights : bool Config.T
@@ -359,8 +359,8 @@
 (* In addition to being easier to read, readable names are often much shorter,
    especially if types are mangled in names. This makes a difference for some
    provers (e.g., E). For these reason, short names are enabled by default. *)
-val atp_readable_names =
-  Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
+val atp_full_names =
+  Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
 val atp_sound_modulo_infiniteness =
   Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness}
                            (K true)
@@ -678,7 +678,7 @@
                      fact_names, typed_helpers, sym_tab) =
                   prepare_atp_problem ctxt format conj_sym_kind prem_kind
                       type_enc false (Config.get ctxt atp_lambda_translation)
-                      (Config.get ctxt atp_readable_names) true hyp_ts concl_t
+                      (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t
                       facts
                 fun weights () = atp_problem_weights atp_problem
                 val full_proof = debug orelse isar_proof