--- 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!