src/Doc/System/Scala.thy

--- a/src/Doc/System/Scala.thy	Sat Nov 28 15:59:24 2020 +0100
+++ b/src/Doc/System/Scala.thy	Sat Nov 28 16:25:29 2020 +0100
@@ -243,8 +243,7 @@
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  Invoke a predefined Scala function that is the identity on type
-  \<^ML_type>\<open>string\<close>:
+  Invoke the predefined Scala function \<^scala_function>\<open>echo\<close>:
 \<close>
 
 ML \<open>