src/Doc/Implementation/Logic.thy

   type variable \<open>\<alpha>\<^sub>s\<close>.
 \<close>
 
 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}
 
   \<^descr> \<^ML>\<open>Thm.extra_shyps\<close>~\<open>thm\<close> determines the extraneous sort hypotheses of
   the given theorem, i.e.\ the sorts that are not present within type

   assumes bad: "\<And>(x::'a) y. x \<noteq> y"
 
 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
   logical significance, this example is merely an instance of \<^emph>\<open>ex falso
   quodlibet consequitur\<close> --- not a collapse of the logical framework!