theory Scratch
  imports Main
begin

ML \<open>
  ProofRewriteRules.mk_of_sort_proof \<^context> [] (\<^typ>\<open>nat\<close>, \<^sort>\<open>order\<close>)
\<close>

end