diff -r b0c81b9a0133 -r e09c53289830 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Wed Dec 10 17:19:25 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Thu Dec 11 18:30:26 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Groebner_Basis.thy
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -165,7 +164,7 @@
 end
 
 interpretation class_semiring: gb_semiring
-    ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
+    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
   proof qed (auto simp add: ring_simps power_Suc)
 
 lemmas nat_arith =
@@ -242,8 +241,8 @@
 end
 
 
-interpretation class_ring: gb_ring ["op +" "op *" "op ^"
-    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
+interpretation class_ring: gb_ring "op +" "op *" "op ^"
+    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
   proof qed simp_all
 
 
@@ -344,7 +343,7 @@
 qed
 
 interpretation class_ringb: ringb
-  ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
+  "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}"
   assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
@@ -360,7 +359,7 @@
 declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
 
 interpretation natgb: semiringb
-  ["op +" "op *" "op ^" "0::nat" "1"]
+  "op +" "op *" "op ^" "0::nat" "1"
 proof (unfold_locales, simp add: ring_simps power_Suc)
   fix w x y z ::"nat"
   { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
@@ -465,7 +464,7 @@
 subsection{* Groebner Bases for fields *}
 
 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)
+  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
 lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"