--- a/src/HOL/Integ/presburger.ML Fri Feb 11 18:51:00 2005 +0100
+++ b/src/HOL/Integ/presburger.ML Sun Feb 13 17:15:14 2005 +0100
@@ -73,7 +73,7 @@
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;
@@ -246,7 +246,7 @@
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]
@@ -313,7 +313,7 @@
"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;