# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1303214563 -3600
# Node ID 59a9c8907a0ff1ea7660c31a6250c6e432057423
# Parent  5c33c4b52ad7119f707500efb9da7a0c22b00d8f
updated

diff -r 5c33c4b52ad7 -r 59a9c8907a0f ProgTutorial/Advanced.thy
--- 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.
 
diff -r 5c33c4b52ad7 -r 59a9c8907a0f progtutorial.pdf
Binary file progtutorial.pdf has changed