--- a/src/HOL/Computational_Algebra/Polynomial.thy Sat Jan 09 00:53:06 2021 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Sat Jan 09 15:56:09 2021 +0100
@@ -3033,7 +3033,7 @@
and algebraic_int_1 [simp, intro]: "algebraic_int 1"
and algebraic_int_numeral [simp, intro]: "algebraic_int (numeral n)"
and algebraic_int_of_nat [simp, intro]: "algebraic_int (of_nat k)"
- and algebraic_int_of_int [simp, intro]: "algebraic_int (of_int k)"
+ and algebraic_int_of_int [simp, intro]: "algebraic_int (of_int m)"
by (simp_all add: int_imp_algebraic_int)
lemma algebraic_int_ii [simp, intro]: "algebraic_int \<i>"