src/HOL/Tools/Presburger/presburger.ML

   | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
   | add_term_typed_consts (_, cs) = cs;
 
 fun term_typed_consts t = add_term_typed_consts(t,[]);
 
-(* Some Types*)
+(* SOME Types*)
 val bT = HOLogic.boolT;
 val iT = HOLogic.intT;
 val binT = HOLogic.binT;
 val nT = HOLogic.natT;
 

     val sg = sign_of_thm st
     (* The Abstraction step *)
     val g' = if a then abstract_pres sg g else g
     (* Transform the term*)
     val (t,np,nh) = prepare_for_presburger sg q g'
-    (* Some simpsets for dealing with mod div abs and nat*)
+    (* SOME simpsets for dealing with mod div abs and nat*)
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
       addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 = HOL_basic_ss

   [Method.add_method ("presburger",
      presburger_args presburger_method,
      "decision procedure for Presburger arithmetic"),
    ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
      {splits = splits, inj_consts = inj_consts, discrete = discrete,
-      presburger = Some (presburger_tac true false)})];
+      presburger = SOME (presburger_tac true false)})];
 
 end;
 
 val presburger_tac = Presburger.presburger_tac true false;