--- a/ProgTutorial/FirstSteps.thy	Sat May 30 23:58:05 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun May 31 00:39:17 2009 +0200
@@ -1009,8 +1009,8 @@
   (FIXME: Explain the following better.)
 
   Occasionally you have to calculate what the ``base'' name of a given
-  constant is. For this you can use the function @{ML [index] extern_const in Sign} or
-  @{ML base_name in Long_Name}. For example:
+  constant is. For this you can use the function @{ML [index] "Sign.extern_const"} or
+  @{ML [index] Long_Name.base_name}. For example:
 
   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}