--- a/ProgTutorial/FirstSteps.thy	Fri May 29 12:15:48 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat May 30 11:12:46 2009 +0200
@@ -4,6 +4,7 @@
 
 chapter {* First Steps *}
 
+
 text {*
   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
   in Isabelle is part of a theory. If you want to follow the code given in
@@ -110,7 +111,7 @@
 
   During development you might find it necessary to inspect some data
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
-  the function @{ML "writeln"}. For example 
+  the function @{ML [indexc] "writeln"}. For example 
 
   @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
 
@@ -716,6 +717,7 @@
   "x x"}
 
   with the raw ML-constructors.
+  
   Sometimes the internal representation of terms can be surprisingly different
   from what you see at the user-level, because the layers of
   parsing/type-checking/pretty printing can be quite elaborate. 
@@ -781,7 +783,7 @@
   \end{readmore}
 *}
 
-section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
+section {* Constructing Terms Manually\label{sec:terms_types_manually} *} 
 
 text {*
   While antiquotations are very convenient for constructing terms, they can
@@ -877,6 +879,16 @@
   @{term \"(\<lambda>x::nat. x)\"}"
   "Free (\"x\", \"nat\")"}
 
+  There are many convenient functions that construct specific HOL-terms. For
+  example @{ML "HOLogic.mk_eq"} constructs an equality out of two terms.
+  The types needed in this equality are calculated from the type of the
+  arguments. For example
+
+@{ML_response_fake [gray,display]
+  "writeln (Syntax.string_of_term @{context}
+   (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))"
+  "True = False"}
+
   \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 
@@ -897,7 +909,11 @@
   in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
   number representing their sum.
   \end{exercise}
-
+*}
+
+section {* Constants *}
+
+text {*
   There are a few subtle issues with constants. They usually crop up when
   pattern matching terms or types, or when constructing them. While it is perfectly ok
   to write the function @{text is_true} as follows
@@ -1003,7 +1019,11 @@
   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 {* Constructing Types Manually *}
+
+text {*
   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 
@@ -1018,6 +1038,13 @@
 ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
 
 text {*
+  If you want to construct a function type with more than one argument
+  type, then you can use @{ML "--->"}.
+*}
+
+ML{*fun make_fun_types tys ty = tys ---> ty *}
+
+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:
@@ -1551,7 +1578,7 @@
   @{text GenericDataFun}:
 *}
 
-ML {*structure MyThmsData = GenericDataFun
+ML{*structure MyThmsData = GenericDataFun
  (type T = thm list
   val empty = []
   val extend = I