diff -r 6d513469f9b2 -r 352c73a689da src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Tue Nov 03 18:11:59 2015 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Nov 04 08:13:49 2015 +0100
@@ -174,14 +174,14 @@
   fixes R (structure) and P (structure)
   defines P_def: "P == UP R"
 
-locale UP_ring = UP + R: ring R
+locale UP_ring = UP + R?: ring R
 
-locale UP_cring = UP + R: cring R
+locale UP_cring = UP + R?: cring R
 
 sublocale UP_cring < UP_ring
   by intro_locales [1] (rule P_def)
 
-locale UP_domain = UP + R: "domain" R
+locale UP_domain = UP + R?: "domain" R
 
 sublocale UP_domain < UP_cring
   by intro_locales [1] (rule P_def)
@@ -457,8 +457,8 @@
 
 end
 
-sublocale UP_ring < P: ring P using UP_ring .
-sublocale UP_cring < P: cring P using UP_cring .
+sublocale UP_ring < P?: ring P using UP_ring .
+sublocale UP_cring < P?: cring P using UP_cring .
 
 
 subsection \<open>Polynomials Form an Algebra\<close>
@@ -1196,8 +1196,6 @@
 
 locale UP_pre_univ_prop = ring_hom_cring + UP_cring
 
-(* FIXME print_locale ring_hom_cring fails *)
-
 locale UP_univ_prop = UP_pre_univ_prop +
   fixes s and Eval
   assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"