diff -r 043ef82000b4 -r 371e4375c994 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Mar 18 03:27:15 2009 +0100
+++ b/CookBook/FirstSteps.thy	Wed Mar 18 18:27:48 2009 +0100
@@ -557,32 +557,31 @@
   While antiquotations are very convenient for constructing terms, they can
   only construct fixed terms (remember they are ``linked'' at compile-time).
   However, you often need to construct terms dynamically. For example, a
-  function that returns the implication @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking
-  @{term P}, @{term Q} and the type @{term "\<tau>"} as arguments can only be
-  written as:
+  function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
+  @{term P} and @{term Q} as arguments can only be written as:
 
 *}
 
-ML{*fun make_imp P Q tau =
+ML{*fun make_imp P Q =
 let
-  val x = Free ("x", tau)
+  val x = Free ("x", @{typ nat})
 in 
   Logic.all x (Logic.mk_implies (P $ x, Q $ x))
 end *}
 
 text {*
-  The reason is that you cannot pass the arguments @{term P}, @{term Q} and 
-  @{term "tau"} into an antiquotation. For example the following does \emph{not} work.
+  The reason is that you cannot pass the arguments @{term P} and @{term Q} 
+  into an antiquotation. For example the following does \emph{not} work.
 *}
 
-ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
+ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
 
 text {*
-  To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 
+  To see this apply @{text "@{term S}"} and @{text "@{term T}"} 
   to both functions. With @{ML make_imp} we obtain the intended term involving 
   the given arguments
 
-  @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" 
+  @{ML_response [display,gray] "make_imp @{term S} @{term T}" 
 "Const \<dots> $ 
   Abs (\"x\", Type (\"nat\",[]),
     Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
@@ -590,48 +589,17 @@
   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}" 
+  @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" 
 "Const \<dots> $ 
   Abs (\"x\", \<dots>,
     Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
   (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda})
-
-
-  Although types of terms can often be inferred, there are many
-  situations where you need to construct types manually, especially  
-  when defining constants. For example the function returning a function 
-  type is as follows:
+*}
 
-*} 
-
-ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
-
-text {* This can be equally written with the combinator @{ML "-->"} as: *}
-
-ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
 text {*
-  A handy function for manipulating terms is @{ML map_types}: it takes a 
-  function and applies it to every type in a term. You can, for example,
-  change every @{typ nat} in a term into an @{typ int} using the function:
-*}
-
-ML{*fun nat_to_int t =
-  (case t of
-     @{typ nat} => @{typ int}
-   | Type (s, ts) => Type (s, map nat_to_int ts)
-   | _ => t)*}
-
-text {*
-  An example as follows:
-
-@{ML_response_fake [display,gray] 
-"map_types nat_to_int @{term \"a = (1::nat)\"}" 
-"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
-           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
-
   \begin{readmore}
   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
@@ -752,8 +720,42 @@
   \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}
+
+  Although types of terms can often be inferred, there are many
+  situations where you need to construct types manually, especially  
+  when defining constants. For example the function returning a function 
+  type is as follows:
+
+*} 
+
+ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
+
+text {* This can be equally written with the combinator @{ML "-->"} as: *}
+
+ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
+
+text {*
+  A handy function for manipulating terms is @{ML map_types}: it takes a 
+  function and applies it to every type in a term. You can, for example,
+  change every @{typ nat} in a term into an @{typ int} using the function:
+*}
+
+ML{*fun nat_to_int t =
+  (case t of
+     @{typ nat} => @{typ int}
+   | Type (s, ts) => Type (s, map nat_to_int ts)
+   | _ => t)*}
+
+text {*
+  An example as follows:
+
+@{ML_response_fake [display,gray] 
+"map_types nat_to_int @{term \"a = (1::nat)\"}" 
+"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
+           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
+
+  (FIXME: readmore about types)
 *}
 
 
@@ -797,7 +799,7 @@
       (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
 end" "0 + 0"}
 
-  In Isabelle not just types need to be certified, but also types. For example, 
+  In Isabelle not just terms need to be certified, but also types. For example, 
   you obtain the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on 
   the ML-level as follows:
 
@@ -1183,23 +1185,23 @@
 text {*
   In the previous section we used \isacommand{setup} in order to make
   a theorem attribute known to Isabelle. What happens behind the scenes
-  is that \isacommand{setup} expects a functions from @{ML_type theory}
-  to @{ML_type theory}: the input theory is the current theory and the 
+  is that \isacommand{setup} expects a functions of type 
+  @{ML_type "theory -> theory"}: the input theory is the current theory and the 
   output the theory where the theory attribute has been stored.
   
   This is a fundamental principle in Isabelle. A similar situation occurs 
   for example with declaring constants. The function that declares a 
-  constant on the ML-level is @{ML Sign.add_consts_i}. Recall that ML-code 
-  needs to be \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.
-  If you write 
+  constant on the ML-level is @{ML Sign.add_consts_i}. 
+  If you write\footnote{Recall that ML-code  needs to be 
+  enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 
 *}  
 
-ML{*Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] @{theory} *}
+ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
 
 text {*
   for declaring the constant @{text "BAR"} with type @{typ nat} and 
   run the code, then you indeed obtain a theory as result. But if you 
-  query the constant with \isacommand{term}
+  query the constant on the Isabelle level using the command \isacommand{term}
 
   \begin{isabelle}
   \isacommand{term}~@{text [quotes] "BAR"}\\
@@ -1212,7 +1214,7 @@
   \isacommand{setup} is for. The constant is properly declared with
 *}
 
-setup %gray {* Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] *}
+setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
 
 text {* 
   Now 
@@ -1266,7 +1268,7 @@
 (*
 setup {*   
   Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
- #> PureThy.add_defs false [((Binding.name "foo_def", 
+ #> PureThy.add_defs false [((@{binding "foo_def"}, 
        Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
  #> snd
 *}