diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Tue Apr 18 12:10:00 2023 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Apr 18 12:23:37 2023 +0200
@@ -949,7 +949,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{define_ML Thm.extra_shyps: "thm -> Sortset.T"} \\
+  @{define_ML Thm.extra_shyps: "thm -> sort list"} \\
   @{define_ML Thm.strip_shyps: "thm -> thm"} \\
   \end{mldecls}
 
@@ -971,7 +971,7 @@
 theorem (in empty) false: False
   using bad by blast
 
-ML_val \<open>\<^assert> (Sortset.dest (Thm.extra_shyps @{thm false}) = [\<^sort>\<open>empty\<close>])\<close>
+ML_val \<open>\<^assert> (Thm.extra_shyps @{thm false} = [\<^sort>\<open>empty\<close>])\<close>
 
 text \<open>
   Thanks to the inference kernel managing sort hypothesis according to their