--- a/src/HOL/Tools/lin_arith.ML Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon Sep 26 07:56:54 2016 +0200
@@ -299,7 +299,7 @@
@{const_name Groups.abs},
@{const_name Groups.minus},
"Int.nat" (*DYNAMIC BINDING!*),
- "Divides.div_class.mod" (*DYNAMIC BINDING!*),
+ @{const_name Rings.modulo},
@{const_name Rings.divide}] a
| _ =>
(if Context_Position.is_visible ctxt then
@@ -467,7 +467,7 @@
(* ?P ((?n::nat) mod (numeral ?k)) =
((numeral ?k = 0 --> ?P ?n) & (~ (numeral ?k = 0) -->
(ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P j))) *)
- | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), (*DYNAMIC BINDING!*) [t1, t2]) =>
+ | (Const (@{const_name Rings.modulo}, Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
let
val rev_terms = rev terms
val zero = Const (@{const_name Groups.zero}, split_type)
@@ -536,7 +536,7 @@
(numeral ?k < 0 -->
(ALL i j.
numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P j))) *)
- | (Const ("Divides.div_class.mod",
+ | (Const (@{const_name Rings.modulo},
Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) =>
let
val rev_terms = rev terms