src/HOL/Probability/ex/Dining_Cryptographers.thy

--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -399,7 +399,7 @@
      (insert n_gt_3, auto simp: dc_crypto intro: exI[of _ "replicate n True"])
 
 sublocale dining_cryptographers_space \<subseteq> information_space "uniform_count_measure dc_crypto" 2
-  by default auto
+  by standard auto
 
 notation (in dining_cryptographers_space)
   mutual_information_Pow ("\<I>'( _ ; _ ')")