--- a/ProgTutorial/FirstSteps.thy	Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Sat Mar 21 12:35:03 2009 +0100
@@ -119,6 +119,22 @@
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 
+  (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling})
+*}
+
+(*
+ML {*
+fun dodgy_fun () = (raise (ERROR "bar"); 1) 
+*}
+
+ML {* set Toplevel.debug *}
+
+ML {* fun f1 () = dodgy_fun () *}
+
+ML {* f1 () *}
+*)
+
+text {*
   Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} 
   or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 
   but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 
@@ -197,10 +213,6 @@
 fun str_of_thms_raw ctxt thms =  
   commas (map (str_of_thm_raw ctxt) thms)*}
 
-text {*
-(FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug})
-*}
-
 section {* Combinators\label{sec:combinators} *}
 
 text {*
@@ -477,6 +489,26 @@
   Again, this way or referencing simpsets makes you independent from additions
   of lemmas to the simpset by the user that potentially cause loops.
 
+  On the ML-level of Isabelle, you often have to work with qualified names;
+  these are strings with some additional information, such positional information
+  and qualifiers. Such bindings can be generated with the antiquotation 
+  @{text "@{bindin \<dots>}"}.
+
+  @{ML_response [display,gray]
+  "@{binding \"name\"}"
+  "name"}
+
+  An example where a binding is needed is the function @{ML define in LocalTheory}.
+  Below this function defines the constant @{term "TrueConj"} as the conjunction
+  @{term "True \<and> True"}.
+*}
+  
+local_setup %gray {* 
+  snd o LocalTheory.define Thm.internalK 
+    ((@{binding "TrueConj"}, NoSyn), 
+     (Attrib.empty_binding, @{term "True \<and> True"})) *}
+
+text {*
   While antiquotations have many applications, they were originally introduced in order 
   to avoid explicit bindings for theorems such as:
 *}
@@ -494,10 +526,6 @@
   kinds of logical elements from th ML-level.
 *}
 
-text {*
-  (FIXME: say something about @{text "@{binding \<dots>}"}
-*}
-
 section {* Terms and Types *}
 
 text {*
@@ -616,14 +644,27 @@
 "Const \<dots> $ 
   Abs (\"x\", \<dots>,
     Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
-               (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
+                (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
-  (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda}, 
+  There are a number of handy functions that are frequently used for 
+  constructing terms. One is the function @{ML list_comb} which a term
+  and a list of terms as argument, and produces as output the term
+  list applied to the term. For example
+
+@{ML_response_fake [display,gray]
+"list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
+"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
+
+  (FIXME: handy functions for constructing terms:  @{ML lambda}, 
   @{ML subst_free})
 *}
 
+ML {* lambda @{term "x::nat"} @{term "P x"}*}
+
 
 text {*
+  As can be seen this function does not take the typing annotation into account.
+
   \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