src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42646 4781fcd53572
parent 42645 242bc53b98e5
child 42647 59142dbfa3ba
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 23:01:22 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 00:10:22 2011 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5    type translated_formula
     1.6  
     1.7 -  val readable_names : bool Unsynchronized.ref
     1.8 +  val readable_names : bool Config.T
     1.9    val fact_prefix : string
    1.10    val conjecture_prefix : string
    1.11    val predicator_base : string
    1.12 @@ -63,7 +63,8 @@
    1.13     names. Also, the logic for generating legal SNARK sort names is only
    1.14     implemented for readable names. Finally, readable names are, well, more
    1.15     readable. For these reason, they are enabled by default. *)
    1.16 -val readable_names = Unsynchronized.ref true
    1.17 +val readable_names =
    1.18 +  Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
    1.19  
    1.20  val type_decl_prefix = "type_"
    1.21  val sym_decl_prefix = "sym_"
    1.22 @@ -983,7 +984,8 @@
    1.23                    map decl_line_for_tff_type (tff_types_in_problem problem))
    1.24            else
    1.25              I)
    1.26 -    val (problem, pool) = problem |> nice_atp_problem (!readable_names)
    1.27 +    val (problem, pool) =
    1.28 +      problem |> nice_atp_problem (Config.get ctxt readable_names)
    1.29    in
    1.30      (problem,
    1.31       case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,