src/HOL/Tools/Meson/meson.ML
changeset 42616 92715b528e78
parent 42455 6702c984bf5a
child 42739 017e5dac8642
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon May 02 13:29:47 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon May 02 16:33:21 2011 +0200
     1.3 @@ -40,19 +40,17 @@
     1.4    val make_meta_clause: thm -> thm
     1.5    val make_meta_clauses: thm list -> thm list
     1.6    val meson_tac: Proof.context -> thm list -> int -> tactic
     1.7 -  val setup : theory -> theory
     1.8  end
     1.9  
    1.10  structure Meson : MESON =
    1.11  struct
    1.12  
    1.13 -val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
    1.14 +val trace = Attrib.setup_config_bool @{binding meson_trace} (K false)
    1.15  
    1.16  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    1.17  
    1.18  val max_clauses_default = 60
    1.19 -val (max_clauses, max_clauses_setup) =
    1.20 -  Attrib.config_int "meson_max_clauses" (K max_clauses_default)
    1.21 +val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K max_clauses_default)
    1.22  
    1.23  (*No known example (on 1-5-2007) needs even thirty*)
    1.24  val iter_deepen_limit = 50;
    1.25 @@ -738,8 +736,4 @@
    1.26      name_thms "MClause#"
    1.27        (distinct Thm.eq_thm_prop (map make_meta_clause ths));
    1.28  
    1.29 -val setup =
    1.30 -  trace_setup
    1.31 -  #> max_clauses_setup
    1.32 -
    1.33  end;