diff -r 0fa87bd86566 -r f0b11413f1c9 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Thu Feb 01 15:12:57 2018 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Thu Feb 01 15:31:25 2018 +0100
@@ -634,7 +634,7 @@
 
   The default is lexicographic ordering of term structure, but this could be
   also changed locally for special applications via @{index_ML
-  Simplifier.set_termless} in Isabelle/ML.
+  Simplifier.set_term_ord} in Isabelle/ML.
 
   \<^medskip>
   Permutative rewrite rules are declared to the Simplifier just like other