diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -163,7 +163,7 @@
 
 end
 
-interpretation class_semiring: gb_semiring
+interpretation class_semiring!: gb_semiring
     "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
   proof qed (auto simp add: ring_simps power_Suc)
 
@@ -242,7 +242,7 @@
 end
 
 
-interpretation class_ring: gb_ring "op +" "op *" "op ^"
+interpretation class_ring!: gb_ring "op +" "op *" "op ^"
     "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
   proof qed simp_all
 
@@ -343,7 +343,7 @@
   thus "b = 0" by blast
 qed
 
-interpretation class_ringb: ringb
+interpretation class_ringb!: ringb
   "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
 proof(unfold_locales, simp add: ring_simps power_Suc, auto)
   fix w x y z ::"'a::{idom,recpower,number_ring}"
@@ -359,7 +359,7 @@
 
 declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
 
-interpretation natgb: semiringb
+interpretation natgb!: semiringb
   "op +" "op *" "op ^" "0::nat" "1"
 proof (unfold_locales, simp add: ring_simps power_Suc)
   fix w x y z ::"nat"
@@ -464,7 +464,7 @@
 
 subsection{* Groebner Bases for fields *}
 
-interpretation class_fieldgb:
+interpretation class_fieldgb!:
   fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
 
 lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp