diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -25,7 +25,7 @@
   proof
     show "emeasure M (space M) \<noteq> \<infinity>" using * by auto
   qed
-  show "subprob_space M" by default fact+
+  show "subprob_space M" by standard fact+
 qed
 
 lemma prob_space_imp_subprob_space: