diff -r e3d0a6a012eb -r 42398b610f86 src/Doc/Implementation/Logic.thy
--- 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