diff -r 4ccb7e635477 -r e68a0b651eb5 src/HOL/Probability/PMF_Impl.thy
--- a/src/HOL/Probability/PMF_Impl.thy	Mon Sep 05 15:00:37 2016 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy	Mon Sep 05 15:47:50 2016 +0200
@@ -527,6 +527,8 @@
 instance by standard (simp add: equal_pmf_def)
 end
 
+definition single :: "'a \<Rightarrow> 'a multiset" where
+"single s = {#s#}"
 
 definition (in term_syntax)
   pmfify :: "('a::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow>