--- a/CookBook/FirstSteps.thy	Fri Mar 06 21:52:17 2009 +0000
+++ b/CookBook/FirstSteps.thy	Sun Mar 08 20:53:00 2009 +0000
@@ -408,17 +408,14 @@
 
 ML{*fun get_thm_names_from_ss simpset =
 let
-  val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
+  val {simps,...} = MetaSimplifier.dest_ss simpset
 in
-  map #name (Net.entries rules)
+  map #1 simps
 end*}
 
 text {*
-  The function @{ML rep_ss in MetaSimplifier} returns a record containing all
-  information about the simpset. The rules of a simpset are stored in a
-  \emph{discrimination net} (a data structure for fast indexing). From this
-  net you can extract the entries using the function @{ML Net.entries}.
-  You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
+  The function @{ML dest_ss in MetaSimplifier} returns a record containing all
+  information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
   in the current simpset. This simpset can be referred to using the antiquotation
   @{text "@{simpset}"}.
 
@@ -444,7 +441,6 @@
   course of this chapter you will learn more about these antiquotations:
   they can simplify Isabelle programming since one can directly access all
   kinds of logical elements from th ML-level.
-
 *}
 
 section {* Terms and Types *}
@@ -710,12 +706,12 @@
 text {*
   Occasional you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML Sign.extern_const} or
-  @{ML NameSpace.base_name}. For example:
+  @{ML 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 NameSpace} always
+  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
   strips off all qualifiers.
 
   \begin{readmore}
@@ -1182,31 +1178,38 @@
 (* FIXME: some code below *)
 
 (*<*)
+(*
 setup {*
- Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] 
+ Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 
 *}
-
+*)
 lemma "bar = (1::nat)"
   oops
 
+(*
 setup {*   
   Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
  #> PureThy.add_defs false [((Binding.name "foo_def", 
        Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
  #> snd
 *}
-
+*)
+(*
 lemma "foo = (1::nat)"
   apply(simp add: foo_def)
   done
 
 thm foo_def
+*)
 (*>*)
 
 section {* Pretty-Printing (TBD) *}
 
 text {*
-  @{ML Pretty.big_list}
+  @{ML Pretty.big_list},
+  @{ML Pretty.brk},
+  @{ML Pretty.block},
+  @{ML Pretty.chunks}
 *}
 
 section {* Misc (TBD) *}