# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1610204169 -3600
# Node ID 9bf36baa8686edc86fbfff4cb51b890ecb67df86
# Parent  918f6c8b1f150e4de178db6b7e2837098e179936
Corrected lemma that was too specific in HOL-Computational_Algebra

diff -r 918f6c8b1f15 -r 9bf36baa8686 src/HOL/Computational_Algebra/Polynomial.thy
--- 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>"