avoid rebinding of existing facts;

--- a/src/HOL/Arith_Tools.thy	Fri Mar 28 19:12:39 2008 +0100
+++ b/src/HOL/Arith_Tools.thy	Fri Mar 28 19:43:54 2008 +0100
@@ -588,7 +588,7 @@
 in
  val field_comp_conv = comp_conv;
  val fieldgb_declaration = 
-  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms}
+  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'}
    {is_const = K numeral_is_const,
     dest_const = K dest_const,
     mk_const = mk_const,

--- a/src/HOL/Groebner_Basis.thy	Fri Mar 28 19:12:39 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Fri Mar 28 19:43:54 2008 +0100
@@ -159,7 +159,7 @@
 qed
 
 
-lemmas gb_semiring_axioms =
+lemmas gb_semiring_axioms' =
   gb_semiring_axioms [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules]
@@ -216,7 +216,7 @@
 end
 *}
 
-declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms} *}
+declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *}
 
 
 locale gb_ring = gb_semiring +
@@ -232,7 +232,7 @@
 
 lemmas ring_rules = neg_mul sub_add
 
-lemmas gb_ring_axioms =
+lemmas gb_ring_axioms' =
   gb_ring_axioms [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules
@@ -247,7 +247,7 @@
   by unfold_locales simp_all
 
 
-declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms} *}
+declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
 
 use "Tools/Groebner_Basis/normalizer.ML"
 
@@ -263,7 +263,7 @@
      and inverse: "inverse x = divide r1 x"
 begin
 
-lemmas gb_field_axioms =
+lemmas gb_field_axioms' =
   gb_field_axioms [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules
@@ -307,9 +307,9 @@
   thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
 qed
 
-declare gb_semiring_axioms [normalizer del]
+declare gb_semiring_axioms' [normalizer del]
 
-lemmas semiringb_axioms = semiringb_axioms [normalizer
+lemmas semiringb_axioms' = semiringb_axioms [normalizer
   semiring ops: semiring_ops
   semiring rules: semiring_rules
   idom rules: noteq_reduce add_scale_eq_noteq]
@@ -320,9 +320,9 @@
   assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
 begin
 
-declare gb_ring_axioms [normalizer del]
+declare gb_ring_axioms' [normalizer del]
 
-lemmas ringb_axioms = ringb_axioms [normalizer
+lemmas ringb_axioms' = ringb_axioms [normalizer
   semiring ops: semiring_ops
   semiring rules: semiring_rules
   ring ops: ring_ops
@@ -356,7 +356,7 @@
   thus "w = x"  by simp
 qed
 
-declaration {* normalizer_funs @{thm class_ringb.ringb_axioms} *}
+declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
 
 interpretation natgb: semiringb
   ["op +" "op *" "op ^" "0::nat" "1"]
@@ -380,14 +380,14 @@
   thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
 qed
 
-declaration {* normalizer_funs @{thm natgb.semiringb_axioms} *}
+declaration {* normalizer_funs @{thm natgb.semiringb_axioms'} *}
 
 locale fieldgb = ringb + gb_field
 begin
 
-declare gb_field_axioms [normalizer del]
+declare gb_field_axioms' [normalizer del]
 
-lemmas fieldgb_axioms = fieldgb_axioms [normalizer
+lemmas fieldgb_axioms' = fieldgb_axioms [normalizer
   semiring ops: semiring_ops
   semiring rules: semiring_rules
   ring ops: ring_ops