--- a/src/Doc/IsarImplementation/ML.thy Wed Feb 27 16:27:44 2013 +0100
+++ b/src/Doc/IsarImplementation/ML.thy Wed Feb 27 17:32:17 2013 +0100
@@ -540,7 +540,7 @@
text {* The primary Isar source language provides facilities to ``open
a window'' to the underlying ML compiler. Especially see the Isar
- commands @{command_ref "use"} and @{command_ref "ML"}: both work the
+ commands @{command_ref "ML_file"} and @{command_ref "ML"}: both work the
same way, only the source text is provided via a file vs.\ inlined,
respectively. Apart from embedding ML into the main theory
definition like that, there are many more commands that refer to ML