--- a/ProgTutorial/Advanced.thy	Fri Jan 01 00:19:11 2010 +0100
+++ b/ProgTutorial/Advanced.thy	Fri Jan 08 21:31:45 2010 +0100
@@ -11,7 +11,7 @@
 (*>*)
 
 
-chapter {* Advanced Isabelle *}
+chapter {* Advanced Isabelle\label{chp:advanced} *}
 
 text {*
    \begin{flushright}
@@ -225,11 +225,71 @@
 
 *}
 
-section {* Managing Name Spaces (TBD) *}
+section {* What Is In an Isabelle Name? (TBD) *}
+
+text {*
+  On the ML-level of Isabelle, you often have to work with qualified names.
+  These are strings with some additional information, such as positional
+  information and qualifiers. Such qualified names can be generated with the
+  antiquotation @{text "@{binding \<dots>}"}. For example
+
+  @{ML_response [display,gray]
+  "@{binding \"name\"}"
+  "name"}
+
+  An example where a qualified name is needed is the function 
+  @{ML_ind define in Local_Theory}.  This function is used below to define 
+  the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
+*}
+
+local_setup %gray {* 
+  Local_Theory.define ((@{binding "TrueConj"}, NoSyn), 
+      (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
+
+text {* 
+  Now querying the definition you obtain:
+
+  \begin{isabelle}
+  \isacommand{thm}~@{text "TrueConj_def"}\\
+  @{text "> "}~@{thm TrueConj_def}
+  \end{isabelle}
+
+  \begin{readmore}
+  The basic operations on bindings are implemented in 
+  @{ML_file "Pure/General/binding.ML"}.
+  \end{readmore}
+
+  \footnote{\bf FIXME give a better example why bindings are important}
+  \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain
+  why @{ML snd} is needed.}
+  \footnote{\bf FIXME: There should probably a separate section on binding, long-names
+  and sign.}
+
+*}
+
 
 ML {* Sign.intern_type @{theory} "list" *}
 ML {* Sign.intern_const @{theory} "prod_fun" *}
 
+text {*
+  \footnote{\bf FIXME: Explain the following better; maybe put in a separate
+  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:
+
+  @{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.
+
+  \begin{readmore}
+  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
+  functions about signatures in @{ML_file "Pure/sign.ML"}.
+  \end{readmore}
+*}
 
 text {* 
   @{ML_ind "Binding.str_of"} returns the string with markup;