diff -r b4da1f2ec73f -r 98f94010d78d src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Sat Jul 27 16:35:51 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Sat Jul 27 16:44:40 2013 +0200
@@ -251,7 +251,7 @@
   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}