--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Jul 02 17:34:45 2014 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Jun 11 14:24:23 2014 +1000
@@ -239,7 +239,7 @@
ultimately
have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} =
{(Some i, zs), (Some i, map Not zs)}"
- using `i < n`
+ using `i < n` [[ hypsubst_thin = true ]]
proof (safe, simp_all add:dc_crypto payer_def)
fix b assume [simp]: "length b = n"
and *: "inversion (Some i, b) = xs" and "b \<noteq> zs"