src/HOL/Algebra/abstract/order.ML

 fun ring_ord a =
   find_index_eq a ["0", "op +", "uminus", "op -", "1", "op *"];
 
 fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
 
-(* SOME code useful for debugging
+(* Some code useful for debugging
 
 val intT = HOLogic.intT;
 val a = Free ("a", intT);
 val b = Free ("b", intT);
 val c = Free ("c", intT);