--- a/ProgTutorial/Advanced.thy	Thu Apr 07 00:25:26 2011 +0100
+++ b/ProgTutorial/Advanced.thy	Tue May 17 18:11:21 2011 +0100
@@ -127,8 +127,8 @@
 
 section {* Contexts (TBD) *}
 
-ML_command "ProofContext.debug := true"
-ML_command "ProofContext.verbose := true"
+ML{*ProofContext.debug*}
+ML{*ProofContext.verbose*}
 
 
 section {* Local Theories (TBD) *}
@@ -276,14 +276,9 @@
   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
-  @{ML_ind  Long_Name.base_name}. For example:
+  constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:
 
-  @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
-
-  The difference between both functions is that @{ML extern_const in Sign} returns
-  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
-  strips off all qualifiers.
+  @{ML_response [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
 
   \begin{readmore}
   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};