src/HOL/Algebra/UnivPoly.thy

 lemma eval_monom_expr:
   assumes a: "a \<in> carrier R"
   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" 
     and mon0_closed: "monom P a 0 \<in> carrier P" 
     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
     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
   also have "\<dots> = \<zero>"
     using a by algebra

   Interpretation now enables to import all theorems and lemmas
   valid in the context of homomorphisms between @{term INTEG} and @{term
   "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]:
   "z \<in> carrier INTEG"
   by (unfold INTEG_def) simp