1.1 --- a/src/HOL/Tools/datatype_prop.ML	Wed Aug 01 16:55:39 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_prop.ML	Wed Aug 01 16:55:40 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature DATATYPE_PROP =
     1.6  sig
     1.7 -  val distinctness_limit : int ConfigOption.T
     1.8 +  val distinctness_limit : int Config.T
     1.9    val distinctness_limit_setup : theory -> theory
    1.10    val indexify_names: string list -> string list
    1.11    val make_tnames: typ list -> string list
    1.12 @@ -41,7 +41,7 @@
    1.13  
    1.14  (*the kind of distinctiveness axioms depends on number of constructors*)
    1.15  val (distinctness_limit, distinctness_limit_setup) =
    1.16 -  ConfigOption.int "datatype_distinctness_limit" 7;
    1.17 +  Attrib.config_int "datatype_distinctness_limit" 7;
    1.18  
    1.19  fun indexify_names names =
    1.20    let
    1.21 @@ -305,7 +305,7 @@
    1.22            end;
    1.23  
    1.24    in map (fn (((_, (_, _, constrs)), T), tname) =>
    1.25 -      if length constrs < ConfigOption.get_thy thy distinctness_limit
    1.26 +      if length constrs < Config.get_thy thy distinctness_limit
    1.27        then make_distincts_1 T constrs else [])
    1.28          ((hd descr) ~~ newTs ~~ new_type_names)
    1.29    end;

     2.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Aug 01 16:55:39 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Aug 01 16:55:40 2007 +0200
     2.3 @@ -526,7 +526,7 @@
     2.4        DatatypeProp.make_distincts new_type_names descr sorts thy5);
     2.5  
     2.6      val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
     2.7 -      if length constrs < ConfigOption.get_thy thy5 DatatypeProp.distinctness_limit
     2.8 +      if length constrs < Config.get_thy thy5 DatatypeProp.distinctness_limit
     2.9        then FewConstrs dists
    2.10        else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
    2.11          constr_rep_thms ~~ rep_congs ~~ distinct_thms);

     3.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Aug 01 16:55:39 2007 +0200
     3.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Aug 01 16:55:40 2007 +0200
     3.3 @@ -14,8 +14,8 @@
     3.4    val arith_discrete: string -> Context.generic -> Context.generic
     3.5    val arith_inj_const: string * typ -> Context.generic -> Context.generic
     3.6    val arith_tactic_add: arith_tactic -> Context.generic -> Context.generic
     3.7 -  val fast_arith_split_limit: int ConfigOption.T
     3.8 -  val fast_arith_neq_limit: int ConfigOption.T
     3.9 +  val fast_arith_split_limit: int Config.T
    3.10 +  val fast_arith_neq_limit: int Config.T
    3.11    val lin_arith_pre_tac: Proof.context -> int -> tactic
    3.12    val fast_arith_tac: Proof.context -> int -> tactic
    3.13    val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
    3.14 @@ -110,24 +110,24 @@
    3.15  
    3.16  val arith_split_add = Thm.declaration_attribute (fn thm =>
    3.17    ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    3.18 -    {splits = insert Thm.eq_thm_prop thm splits,
    3.19 +    {splits = update Thm.eq_thm_prop thm splits,
    3.20       inj_consts = inj_consts, discrete = discrete, tactics = tactics}));
    3.21  
    3.22  fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    3.23    {splits = splits, inj_consts = inj_consts,
    3.24 -   discrete = insert (op =) d discrete, tactics = tactics});
    3.25 +   discrete = update (op =) d discrete, tactics = tactics});
    3.26  
    3.27  fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    3.28 -  {splits = splits, inj_consts = insert (op =) c inj_consts,
    3.29 +  {splits = splits, inj_consts = update (op =) c inj_consts,
    3.30     discrete = discrete, tactics= tactics});
    3.31  
    3.32  fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    3.33    {splits = splits, inj_consts = inj_consts, discrete = discrete,
    3.34 -   tactics = insert eq_arith_tactic tac tactics});
    3.35 +   tactics = update eq_arith_tactic tac tactics});
    3.36  
    3.37  
    3.38 -val (fast_arith_split_limit, setup1) = ConfigOption.int "fast_arith_split_limit" 9;
    3.39 -val (fast_arith_neq_limit, setup2) = ConfigOption.int "fast_arith_neq_limit" 9;
    3.40 +val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9;
    3.41 +val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9;
    3.42  val setup_options = setup1 #> setup2;
    3.43  
    3.44  
    3.45 @@ -382,7 +382,7 @@
    3.46    val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
    3.47    val cmap       = Splitter.cmap_of_split_thms split_thms
    3.48    val splits     = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms)
    3.49 -  val split_limit = ConfigOption.get ctxt fast_arith_split_limit
    3.50 +  val split_limit = Config.get ctxt fast_arith_split_limit
    3.51  in
    3.52    if length splits > split_limit then
    3.53     (tracing ("fast_arith_split_limit exceeded (current value is " ^
    3.54 @@ -741,7 +741,7 @@
    3.55          val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
    3.56          val cmap = Splitter.cmap_of_split_thms split_thms
    3.57          val splits = Splitter.split_posns cmap thy Ts concl
    3.58 -        val split_limit = ConfigOption.get ctxt fast_arith_split_limit
    3.59 +        val split_limit = Config.get ctxt fast_arith_split_limit
    3.60        in
    3.61          if length splits > split_limit then no_tac
    3.62          else split_tac split_thms i

     4.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Aug 01 16:55:39 2007 +0200
     4.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Aug 01 16:55:40 2007 +0200
     4.3 @@ -62,7 +62,7 @@
     4.4  
     4.5    (*the limit on the number of ~= allowed; because each ~= is split
     4.6      into two cases, this can lead to an explosion*)
     4.7 -  val fast_arith_neq_limit: int ConfigOption.T
     4.8 +  val fast_arith_neq_limit: int Config.T
     4.9  end;
    4.10  (*
    4.11  decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
    4.12 @@ -715,7 +715,7 @@
    4.13      val Hs' = Hs @ [LA_Logic.neg_prop concl]
    4.14      fun is_neq NONE                 = false
    4.15        | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
    4.16 -    val neq_limit = ConfigOption.get ctxt LA_Data.fast_arith_neq_limit;
    4.17 +    val neq_limit = Config.get ctxt LA_Data.fast_arith_neq_limit;
    4.18    in
    4.19      if count is_neq (map (LA_Data.decomp ctxt) Hs') > neq_limit then
    4.20       (trace_msg ("fast_arith_neq_limit exceeded (current value is " ^

     5.1 --- a/src/Provers/blast.ML	Wed Aug 01 16:55:39 2007 +0200
     5.2 +++ b/src/Provers/blast.ML	Wed Aug 01 16:55:40 2007 +0200
     5.3 @@ -76,7 +76,7 @@
     5.4      | $  of term*term;
     5.5    type branch
     5.6    val depth_tac         : claset -> int -> int -> tactic
     5.7 -  val depth_limit: int ConfigOption.T
     5.8 +  val depth_limit       : int Config.T
     5.9    val blast_tac         : claset -> int -> tactic
    5.10    val Blast_tac         : int -> tactic
    5.11    val setup             : theory -> theory
    5.12 @@ -1274,10 +1274,10 @@
    5.13  (*Public version with fixed depth*)
    5.14  fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
    5.15  
    5.16 -val (depth_limit, setup_depth_limit) = ConfigOption.global_int "blast_depth_limit" 20;
    5.17 +val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20;
    5.18  
    5.19  fun blast_tac cs i st =
    5.20 -    ((DEEPEN (1, ConfigOption.get_thy (Thm.theory_of_thm st) depth_limit)
    5.21 +    ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
    5.22          (timing_depth_tac (start_timing ()) cs) 0) i
    5.23       THEN flexflex_tac) st
    5.24      handle TRANS s =>