diff -r 83f36a1c62f2 -r 3fb9f820a294 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Fri Mar 06 16:12:16 2009 +0000
+++ b/CookBook/FirstSteps.thy	Fri Mar 06 21:52:17 2009 +0000
@@ -555,19 +555,18 @@
   the given arguments
 
   @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" 
-    "Const \<dots> $ 
-    Abs (\"x\", Type (\"nat\",[]),
-      Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 
-                  (Free (\"T\",\<dots>) $ \<dots>))"}
+"Const \<dots> $ 
+  Abs (\"x\", Type (\"nat\",[]),
+    Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
 
   whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} 
   and @{text "Q"} from the antiquotation.
 
   @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" 
-    "Const \<dots> $ 
-    Abs (\"x\", \<dots>,
-      Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
-                  (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
+"Const \<dots> $ 
+  Abs (\"x\", \<dots>,
+    Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
+               (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
   Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
@@ -576,7 +575,7 @@
 
 *} 
 
-ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
+ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
 
 text {* This can be equally written with the combinator @{ML "-->"} as: *}
 
@@ -708,25 +707,24 @@
   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
   | is_nil_or_all _ = false *}
 
-(*
 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 Sign.base_name}. For example:
+  @{ML NameSpace.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 Sign} always
+  the smallest name that is still unique, whereas @{ML base_name in NameSpace} always
   strips off all qualifiers.
 
-  (FIXME: These are probably now NameSpace functions)
-
   \begin{readmore}
-  FIXME: Find the right files to do with naming.
+  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
+  functions about signatures in @{ML_file "Pure/sign.ML"}.
+  
   \end{readmore}
 *}
-*)
+
 
 section {* Type-Checking *}
 
@@ -844,6 +842,8 @@
   type inference are implemented in @{ML_file "Pure/type.ML"} and 
   @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
+
+  (FIXME: say something about sorts)
 *}