diff -r 00d04a562df1 -r bd786c37af84 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 21:29:34 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy	Fri Feb 20 23:46:03 2009 +0100
@@ -448,8 +448,8 @@
 declare zmod_zminus2[algebra]
 declare zdiv_zero[algebra]
 declare zmod_zero[algebra]
-declare zmod_1[algebra]
-declare zdiv_1[algebra]
+declare mod_by_1[algebra]
+declare div_by_1[algebra]
 declare zmod_minus1_right[algebra]
 declare zdiv_minus1_right[algebra]
 declare mod_div_trivial[algebra]