src/HOL/IntDiv.thy

 lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
 by(simp add: mult_commute zmod_zdiv_equality[symmetric])
 
 text {* Tool setup *}
 
-ML_setup {*
+ML {*
 local 
 
 structure CancelDivMod = CancelDivModFun(
 struct
   val div_name = @{const_name Divides.div};