1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:07:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 30 16:07:45 2011 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4    val problem_prefix : string Config.T
     1.5    val measure_run_time : bool Config.T
     1.6    val atp_lambda_translation : string Config.T
     1.7 -  val atp_readable_names : bool Config.T
     1.8 +  val atp_full_names : bool Config.T
     1.9    val atp_sound_modulo_infiniteness : bool Config.T
    1.10    val smt_triggers : bool Config.T
    1.11    val smt_weights : bool Config.T
    1.12 @@ -359,8 +359,8 @@
    1.13  (* In addition to being easier to read, readable names are often much shorter,
    1.14     especially if types are mangled in names. This makes a difference for some
    1.15     provers (e.g., E). For these reason, short names are enabled by default. *)
    1.16 -val atp_readable_names =
    1.17 -  Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
    1.18 +val atp_full_names =
    1.19 +  Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
    1.20  val atp_sound_modulo_infiniteness =
    1.21    Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness}
    1.22                             (K true)
    1.23 @@ -678,7 +678,7 @@
    1.24                       fact_names, typed_helpers, sym_tab) =
    1.25                    prepare_atp_problem ctxt format conj_sym_kind prem_kind
    1.26                        type_enc false (Config.get ctxt atp_lambda_translation)
    1.27 -                      (Config.get ctxt atp_readable_names) true hyp_ts concl_t
    1.28 +                      (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t
    1.29                        facts
    1.30                  fun weights () = atp_problem_weights atp_problem
    1.31                  val full_proof = debug orelse isar_proof