diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -168,7 +168,7 @@
 
 interpretation class_semiring: gb_semiring
     ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
-  by unfold_locales (auto simp add: ring_simps power_Suc)
+  proof qed (auto simp add: ring_simps power_Suc)
 
 lemmas nat_arith =
   add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
@@ -244,7 +244,7 @@
 
 interpretation class_ring: gb_ring ["op +" "op *" "op ^"
     "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
-  by unfold_locales simp_all
+  proof qed simp_all
 
 
 declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}