src/HOL/arith_data.ML

 end;
 
 
 (* arith theory data *)
 
-structure ArithDataArgs =
+structure ArithTheoryDataArgs =
 struct
   val name = "HOL/arith";
   type T = {splits: thm list, discrete: (string * bool) list};
 
   val empty = {splits = [], discrete = []};

    {splits = Drule.merge_rules (splits1, splits2),
     discrete = merge_alists discrete1 discrete2};
   fun print _ _ = ();
 end;
 
-structure ArithData = TheoryDataFun(ArithDataArgs);
-
-fun arith_split_add (thy, thm) = (ArithData.map (fn {splits, discrete} =>
+structure ArithTheoryData = TheoryDataFun(ArithTheoryDataArgs);
+
+fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits, discrete} =>
   {splits = thm :: splits, discrete = discrete}) thy, thm);
 
-fun arith_discrete d = ArithData.map (fn {splits, discrete} =>
+fun arith_discrete d = ArithTheoryData.map (fn {splits, discrete} =>
   {splits = splits, discrete = d :: discrete});
 
 
 structure LA_Data_Ref: LIN_ARITH_DATA =
 struct

 fun decomp2 discrete (_$(Const(rel,T)$lhs$rhs)) = decomp1 discrete (T,(rel,lhs,rhs))
   | decomp2 discrete (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
       negate(decomp1 discrete (T,(rel,lhs,rhs)))
   | decomp2 discrete _ = None
 
-val decomp = decomp2 o #discrete o ArithData.get_sg;
+val decomp = decomp2 o #discrete o ArithTheoryData.get_sg;
 
 end;
 
 
 structure Fast_Arith =

  Fast_Arith.setup @
  [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset = _} =>
    {add_mono_thms = add_mono_thms @ add_mono_thms_nat,
     lessD = lessD @ [Suc_leI],
     simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
-  ArithData.init, arith_discrete ("nat", true)];
+  ArithTheoryData.init, arith_discrete ("nat", true)];
 
 end;
 
 
 local

    elimination of min/max can be optimized:
    (max m n + k <= r) = (m+k <= r & n+k <= r)
    (l <= min m n + k) = (l <= m+k & l <= n+k)
 *)
 fun arith_tac i st =
-  refute_tac (K true) (REPEAT o split_tac (#splits (ArithData.get_sg (Thm.sign_of_thm st))))
+  refute_tac (K true) (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
              ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st;
 
 fun arith_method prems =
   Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));