--- a/src/Doc/Implementation/Logic.thy Wed Apr 01 22:08:06 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy Wed Apr 01 22:40:07 2015 +0200
@@ -982,7 +982,7 @@
theorem (in empty) false: False
using bad by blast
-ML \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
+ML_val \<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