diff -r 3c576c7f9731 -r 1bd1d8492931 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Mon Apr 04 15:53:56 2016 +0200
+++ b/src/Doc/System/Environment.thy	Mon Apr 04 16:14:22 2016 +0200
@@ -395,8 +395,8 @@
 
   The user is connected to the raw ML toplevel loop: this is neither
   Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
-  relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
-  use_thys}.
+  relevant ML commands at this stage are @{ML use} (for ML files) and
+  @{ML use_thy} (for theory files).
 \<close>