# HG changeset patch
# User wenzelm
# Date 1374936280 -7200
# Node ID 98f94010d78d3d8525046289a135389dbb8be8b2
# Parent  b4da1f2ec73fb664ae114090c63dfebc18548fe8
tuned;

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}