simplified internal Config interface;

--- a/src/HOL/Tools/datatype_prop.ML	Wed Aug 01 16:55:39 2007 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Wed Aug 01 16:55:40 2007 +0200
@@ -7,7 +7,7 @@
 
 signature DATATYPE_PROP =
 sig
-  val distinctness_limit : int ConfigOption.T
+  val distinctness_limit : int Config.T
   val distinctness_limit_setup : theory -> theory
   val indexify_names: string list -> string list
   val make_tnames: typ list -> string list
@@ -41,7 +41,7 @@
 
 (*the kind of distinctiveness axioms depends on number of constructors*)
 val (distinctness_limit, distinctness_limit_setup) =
-  ConfigOption.int "datatype_distinctness_limit" 7;
+  Attrib.config_int "datatype_distinctness_limit" 7;
 
 fun indexify_names names =
   let
@@ -305,7 +305,7 @@
           end;
 
   in map (fn (((_, (_, _, constrs)), T), tname) =>
-      if length constrs < ConfigOption.get_thy thy distinctness_limit
+      if length constrs < Config.get_thy thy distinctness_limit
       then make_distincts_1 T constrs else [])
         ((hd descr) ~~ newTs ~~ new_type_names)
   end;

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

--- a/src/HOL/Tools/lin_arith.ML	Wed Aug 01 16:55:39 2007 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Aug 01 16:55:40 2007 +0200
@@ -14,8 +14,8 @@
   val arith_discrete: string -> Context.generic -> Context.generic
   val arith_inj_const: string * typ -> Context.generic -> Context.generic
   val arith_tactic_add: arith_tactic -> Context.generic -> Context.generic
-  val fast_arith_split_limit: int ConfigOption.T
-  val fast_arith_neq_limit: int ConfigOption.T
+  val fast_arith_split_limit: int Config.T
+  val fast_arith_neq_limit: int Config.T
   val lin_arith_pre_tac: Proof.context -> int -> tactic
   val fast_arith_tac: Proof.context -> int -> tactic
   val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
@@ -110,24 +110,24 @@
 
 val arith_split_add = Thm.declaration_attribute (fn thm =>
   ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
-    {splits = insert Thm.eq_thm_prop thm splits,
+    {splits = update Thm.eq_thm_prop thm splits,
      inj_consts = inj_consts, discrete = discrete, tactics = tactics}));
 
 fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
   {splits = splits, inj_consts = inj_consts,
-   discrete = insert (op =) d discrete, tactics = tactics});
+   discrete = update (op =) d discrete, tactics = tactics});
 
 fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
-  {splits = splits, inj_consts = insert (op =) c inj_consts,
+  {splits = splits, inj_consts = update (op =) c inj_consts,
    discrete = discrete, tactics= tactics});
 
 fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
   {splits = splits, inj_consts = inj_consts, discrete = discrete,
-   tactics = insert eq_arith_tactic tac tactics});
+   tactics = update eq_arith_tactic tac tactics});
 
 
-val (fast_arith_split_limit, setup1) = ConfigOption.int "fast_arith_split_limit" 9;
-val (fast_arith_neq_limit, setup2) = ConfigOption.int "fast_arith_neq_limit" 9;
+val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9;
+val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9;
 val setup_options = setup1 #> setup2;
 
 
@@ -382,7 +382,7 @@
   val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
   val cmap       = Splitter.cmap_of_split_thms split_thms
   val splits     = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms)
-  val split_limit = ConfigOption.get ctxt fast_arith_split_limit
+  val split_limit = Config.get ctxt fast_arith_split_limit
 in
   if length splits > split_limit then
    (tracing ("fast_arith_split_limit exceeded (current value is " ^
@@ -741,7 +741,7 @@
         val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
         val cmap = Splitter.cmap_of_split_thms split_thms
         val splits = Splitter.split_posns cmap thy Ts concl
-        val split_limit = ConfigOption.get ctxt fast_arith_split_limit
+        val split_limit = Config.get ctxt fast_arith_split_limit
       in
         if length splits > split_limit then no_tac
         else split_tac split_thms i

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

--- a/src/Provers/blast.ML	Wed Aug 01 16:55:39 2007 +0200
+++ b/src/Provers/blast.ML	Wed Aug 01 16:55:40 2007 +0200
@@ -76,7 +76,7 @@
     | $  of term*term;
   type branch
   val depth_tac         : claset -> int -> int -> tactic
-  val depth_limit: int ConfigOption.T
+  val depth_limit       : int Config.T
   val blast_tac         : claset -> int -> tactic
   val Blast_tac         : int -> tactic
   val setup             : theory -> theory
@@ -1274,10 +1274,10 @@
 (*Public version with fixed depth*)
 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
 
-val (depth_limit, setup_depth_limit) = ConfigOption.global_int "blast_depth_limit" 20;
+val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20;
 
 fun blast_tac cs i st =
-    ((DEEPEN (1, ConfigOption.get_thy (Thm.theory_of_thm st) depth_limit)
+    ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
         (timing_depth_tac (start_timing ()) cs) 0) i
      THEN flexflex_tac) st
     handle TRANS s =>