--- a/ProgTutorial/FirstSteps.thy	Sat Aug 01 08:59:41 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sun Aug 02 08:44:41 2009 +0200
@@ -852,7 +852,7 @@
   \end{readmore}
 *}
 
-section {* Constructing Terms Manually\label{sec:terms_types_manually} *} 
+section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
 
 text {*
   While antiquotations are very convenient for constructing terms, they can
@@ -904,18 +904,23 @@
 
 @{ML_response_fake [display,gray]
 "let
-  val t = @{term \"P::nat\"}
+  val trm = @{term \"P::nat\"}
   val args = [@{term \"True\"}, @{term \"False\"}]
 in
-  list_comb (t, args)
+  list_comb (trm, args)
 end"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 
   Another handy function is @{ML [index] lambda}, which abstracts a variable 
   in a term. For example
-  
+
   @{ML_response_fake [display,gray]
-  "lambda @{term \"x::nat\"} @{term \"(P::nat \<Rightarrow> bool) x\"}"
+"let
+  val x_nat = @{term \"x::nat\"}
+  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+in
+  lambda x_nat trm
+end"
   "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
   In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
@@ -926,10 +931,15 @@
   as in
 
   @{ML_response_fake [display,gray]
-  "lambda @{term \"x::nat\"} @{term \"(P::bool \<Rightarrow> bool) x\"}"
-  "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Free (\"x\", \"bool\"))"}
-
-  then the variable @{text "Free (\"x\", \"bool\")"} is \emph{not} abstracted. 
+"let
+  val x_int = @{term \"x::int\"}
+  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+in
+  lambda x_int trm
+end"
+  "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
+
+  then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. 
   This is a fundamental principle
   of Church-style typing, where variables with the same name still differ, if they 
   have different type.
@@ -943,7 +953,7 @@
 "let
   val s1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
   val s2 = (@{term \"x::nat\"}, @{term \"True\"})
-  val trm =  @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
+  val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
 in
   subst_free [s1, s2] trm
 end"
@@ -967,8 +977,11 @@
   arguments. For example
 
 @{ML_response_fake [gray,display]
-  "writeln (Syntax.string_of_term @{context}
-   (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))"
+"let
+  val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
+in
+  writeln (Syntax.string_of_term @{context} eq)
+end"
   "True = False"}
 *}
 
@@ -977,14 +990,11 @@
   Most of the HOL-specific operations on terms and types are defined 
   in @{ML_file "HOL/Tools/hologic.ML"}.
   \end{readmore}
-*}
-
-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
+
+  When constructing terms manually, 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
 *}
 
 ML{*fun is_true @{term True} = true
@@ -1108,11 +1118,7 @@
   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 
@@ -1166,12 +1172,12 @@
   call them as follows
 
   @{ML_response [gray,display]
-  "Term.add_tfrees @{term \"(a,b)\"} []"
+  "Term.add_tfrees @{term \"(a, b)\"} []"
   "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
 
   The reason for this definition is that @{ML add_tfrees in Term} can
   be easily folded over a list of terms. Similarly for all functions
-  named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}.
+  named @{text "add_*"} in @{ML_file "Pure/term.ML"}.
 
 *}
 
@@ -2252,4 +2258,6 @@
 
 ML {*Datatype.get_info @{theory} "List.list"*}
 
+section {* Name Space(TBD) *}
+
 end