--- a/ProgTutorial/Advanced.thy	Thu Apr 07 00:25:26 2011 +0100
+++ b/ProgTutorial/Advanced.thy	Tue Apr 19 13:02:43 2011 +0100
@@ -276,12 +276,12 @@
   section and link with the comment in the antiquotation section.}
 
   Occasionally you have to calculate what the ``base'' name of a given
-  constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or
+  constant is. For this you can use the function @{ML_ind "ProofContext.extern_const"} or
   @{ML_ind  Long_Name.base_name}. For example:
 
-  @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
+  @{ML_response [display,gray] "ProofContext.extern_const @{context} \"List.list.Nil\"" "\"Nil\""}
 
-  The difference between both functions is that @{ML extern_const in Sign} returns
+  The difference between both functions is that @{ML extern_const in ProofContext} returns
   the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
   strips off all qualifiers.