diff -r 310a3f2f0e7e -r da7b40aa2215 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Fri Apr 16 12:51:37 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Fri Apr 16 12:51:57 2010 +0200
@@ -334,7 +334,7 @@
   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML
   Var}, @{ML Const}, @{ML Abs}, @{ML "op $"}.
 
-  \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
+  \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text
   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
   on type @{ML_type term}; raw datatype equality should only be used
   for operations related to parsing or printing!