src/Provers/Arith/fast_lin_arith.ML

   val pre_tac: Proof.context -> int -> tactic
   val number_of: IntInf.int * typ -> term
 
   (*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)
    where Rel is one of "<", "~<", "<=", "~<=" and "=" and
          p (q, respectively) is the decomposition of the sum term x

     (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *)
     (* theorem/tactic level                                             *)
     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 " ^
         string_of_int neq_limit ^ ")"); NONE)
     else