diff -r 0ad86d5b3bc3 -r 4a174bea55e2 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Tue Mar 28 17:51:21 2023 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Mar 28 17:59:54 2023 +0200
@@ -949,7 +949,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{define_ML Thm.extra_shyps: "thm -> sort list"} \\
+  @{define_ML Thm.extra_shyps: "thm -> Sortset.T"} \\
   @{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> (Thm.extra_shyps @{thm false} = [\<^sort>\<open>empty\<close>])\<close>
+ML_val \<open>\<^assert> (Sortset.dest (Thm.extra_shyps @{thm false}) = [\<^sort>\<open>empty\<close>])\<close>
 
 text \<open>
   Thanks to the inference kernel managing sort hypothesis according to their