src/Doc/Implementation/Logic.thy

--- a/src/Doc/Implementation/Logic.thy	Sun Jul 01 12:37:24 2018 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sun Jul 01 12:38:37 2018 +0200
@@ -862,13 +862,9 @@
 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>