--- a/ProgTutorial/FirstSteps.thy	Wed Apr 08 10:40:16 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 08 13:42:18 2009 +0100
@@ -38,7 +38,7 @@
 \end{graybox}
 \end{isabelle}
 
-  Like normal Isabelle proof scripts, \isacommand{ML}-commands can be
+  Like normal Isabelle scripts, \isacommand{ML}-commands can be
   evaluated by using the advance and undo buttons of your Isabelle
   environment. The code inside the \isacommand{ML}-command can also contain
   value and function bindings, for example