src/Doc/IsarImplementation/ML.thy

 
   \item certified types are called @{ML_text cT}, rarely @{ML_text
   T}, with variants as for types
 
   \item certified terms are called @{ML_text ct}, rarely @{ML_text
-  t}, with variants as for terms
+  t}, with variants as for terms (never @{ML_text ctrm})
 
   \item theorems are called @{ML_text th}, or @{ML_text thm}
 
   \end{itemize}