src/Doc/Implementation/Logic.thy

--- a/src/Doc/Implementation/Logic.thy	Fri Jun 29 14:19:52 2018 +0200
+++ b/src/Doc/Implementation/Logic.thy	Fri Jun 29 15:54:41 2018 +0200
@@ -862,9 +862,13 @@
 class empty =
   assumes bad: "\<And>(x::'a) y. x \<noteq> y"
 
+declare [[pending_shyps]]
+
 theorem (in empty) false: False
   using bad by blast
 
+declare [[pending_shyps = false]]
+
 ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
 
 text \<open>