# HG changeset patch
# User wenzelm
# Date 1204749239 -3600
# Node ID 51f8a696cd8da298430ef2bee3d5546572003e3a
# Parent  d3363a8547083075bd7526b240298fd513631435
explicit referencing of background facts;

diff -r d3363a854708 -r 51f8a696cd8d src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Mar 05 21:24:07 2008 +0100
+++ b/src/HOL/Algebra/Ring.thy	Wed Mar 05 21:33:59 2008 +0100
@@ -362,7 +362,7 @@
 
 lemma (in ring) is_ring:
   "ring R"
-  by fact
+  by (rule ring_axioms)
 
 lemmas ring_record_simps = monoid_record_simps ring.simps
 
@@ -399,7 +399,7 @@
   by (auto intro!: comm_monoidI m_assoc m_comm)
 
 lemma (in cring) is_cring:
-  "cring R" by fact
+  "cring R" by (rule cring_axioms)
 
 
 subsubsection {* Normaliser for Rings *}
diff -r d3363a854708 -r 51f8a696cd8d src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Mar 05 21:24:07 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Mar 05 21:33:59 2008 +0100
@@ -1229,7 +1229,7 @@
   shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
 proof -
   interpret UP_univ_prop [R S h P s _]
-    using `UP_pre_univ_prop R S h` P_def R S
+    using UP_pre_univ_prop_axioms P_def R S
     by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
   from R
   show ?thesis by (rule Eval_monom)