diff -r bb20f11dd842 -r 1bf7b186542e src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Mon Nov 09 15:48:17 2015 +0100
@@ -97,7 +97,7 @@
     by simp
 qed (force simp: generator.simps prod_emb_empty[symmetric])
 
-interpretation generator!: algebra "space (PiM I M)" generator
+interpretation generator: algebra "space (PiM I M)" generator
   by (rule algebra_generator)
 
 lemma sets_PiM_generator: "sets (PiM I M) = sigma_sets (space (PiM I M)) generator"
@@ -407,7 +407,7 @@
 definition CI :: "nat set \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
   "CI J = distr (C 0 (up_to J) (\<lambda>x. undefined)) (PiM J M) (\<lambda>f. restrict f J)"
 
-sublocale PF!: projective_family UNIV CI
+sublocale PF: projective_family UNIV CI
   unfolding projective_family_def
 proof safe
   show "finite J \<Longrightarrow> prob_space (CI J)" for J
@@ -460,7 +460,7 @@
   also have "\<dots> \<le> (INF i. C 0 i (\<lambda>x. undefined) (X i))"
   proof (intro INF_greatest)
     fix n
-    interpret C!: prob_space "C 0 n (\<lambda>x. undefined)"
+    interpret C: prob_space "C 0 n (\<lambda>x. undefined)"
       by (rule prob_space_C) simp
     show "(INF i. CI (J i) (X' i)) \<le> C 0 n (\<lambda>x. undefined) (X n)"
     proof cases
@@ -606,9 +606,9 @@
       using count by (auto simp: t_def)
     then have inj_t_J: "inj_on t (J i)" for i
       by (rule subset_inj_on) auto
-    interpret IT!: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
+    interpret IT: Ionescu_Tulcea "\<lambda>i \<omega>. M (f i)" "\<lambda>i. M (f i)"
       by standard auto
-    interpret Mf!: product_prob_space "\<lambda>x. M (f x)" UNIV
+    interpret Mf: product_prob_space "\<lambda>x. M (f x)" UNIV
       by standard
     have C_eq_PiM: "IT.C 0 n (\<lambda>_. undefined) = PiM {0..<n} (\<lambda>x. M (f x))" for n
     proof (induction n)