# HG changeset patch
# User ballarin
# Date 1229693477 -3600
# Node ID 3593802c9cf184f3fabeb300c68ec1ab73b2fa88
# Parent  19728ee2b1bab854240f1bee84649c8478eb02e8
More porting to new locales.

diff -r 19728ee2b1ba -r 3593802c9cf1 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Fri Dec 19 14:31:07 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Fri Dec 19 14:31:17 2008 +0100
@@ -17,10 +17,10 @@
   notes hom_mult [simp] = ring_hom_mult [OF homh]
     and hom_one [simp] = ring_hom_one [OF homh]
 
-sublocale ring_hom_cring \<subseteq> ring_hom_ring
+sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
   proof qed (rule homh)
 
-sublocale ring_hom_ring \<subseteq> abelian_group_hom R S
+sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
 apply (rule abelian_group_homI)
   apply (rule R.is_abelian_group)
  apply (rule S.is_abelian_group)
diff -r 19728ee2b1ba -r 3593802c9cf1 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Dec 19 14:31:07 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Dec 19 14:31:17 2008 +0100
@@ -1773,7 +1773,7 @@
   shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
   (is "eval R R id a ?g = _")
 proof -
-  interpret UP_pre_univ_prop R R id P proof qed simp
+  interpret UP_pre_univ_prop R R id proof qed simp
   have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
   interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
   have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
@@ -1782,8 +1782,8 @@
     using a R.a_inv_closed by auto
   have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
     unfolding P.minus_eq [OF mon1_closed mon0_closed]
-    unfolding R_S_h.hom_add [OF mon1_closed min_mon0_closed]
-    unfolding R_S_h.hom_a_inv [OF mon0_closed] 
+    unfolding hom_add [OF mon1_closed min_mon0_closed]
+    unfolding hom_a_inv [OF mon0_closed] 
     using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
   also have "\<dots> = a \<ominus> a"
     using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
@@ -1886,7 +1886,7 @@
   "UP INTEG"} globally.
 *}
 
-interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
+interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
   using INTEG_id_eval by simp_all
 
 lemma INTEG_closed [intro, simp]: