--- a/src/Doc/Implementation/Logic.thy Mon Oct 20 22:46:17 2014 +0200
+++ b/src/Doc/Implementation/Logic.thy Mon Oct 20 23:17:28 2014 +0200
@@ -981,9 +981,7 @@
theorem (in empty) false: False
using bad by blast
-ML \<open>
- @{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])
-\<close>
+ML \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
text \<open>Thanks to the inference kernel managing sort hypothesis
according to their logical significance, this example is merely an