--- a/src/HOL/Predicate.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Predicate.thy Tue Sep 03 01:12:40 2013 +0200
@@ -225,9 +225,9 @@
"\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
proof -
assume assm: "\<exists>!x. eval A x"
- then obtain x where "eval A x" ..
- moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
- ultimately show ?thesis by simp
+ then obtain x where x: "eval A x" ..
+ with assm have "singleton dfault A = x" by (rule singleton_eqI)
+ with x show ?thesis by simp
qed
lemma single_singleton: