diff -r 978c00c20a59 -r 8ada79014cb2 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:27:49 2012 +0200
+++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 15:34:04 2012 +0200
@@ -62,8 +62,8 @@
 declare mod_0[algebra]
 declare mod_by_1[algebra]
 declare div_by_1[algebra]
-declare zmod_minus1_right[algebra]
-declare zdiv_minus1_right[algebra]
+declare mod_minus1_right[algebra]
+declare div_minus1_right[algebra]
 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
 declare mod_mult_self2_is_0[algebra]