--- a/ProgTutorial/First_Steps.thy	Thu Oct 27 18:11:52 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Sat Oct 29 13:17:12 2011 +0100
@@ -644,34 +644,34 @@
   "acc_incs 1 ||>> (fn x => (x, x + 2))"
   "(((((\"\", 1), 2), 3), 4), 6)"}
 
-  An example for this combinator is for example the following code
+  A more realistic example for this combinator is the following code
 *}
 
-ML {*
-val (((one_def, two_def), three_def), ctxt') = 
+ML{*val (((one_def, two_def), three_def), ctxt') = 
   @{context}
   |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) 
   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
-ML {*
-  @{context}
-  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) 
-  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
-ML {*
-  val ((((One, One_thm), (Two, Two_thm)), (Three, Three_thm)), _)) = 
-  @{context}
-  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
+  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
 
 text {*
+  where we make three definitions, namely @{term "one \<equiv> 1::nat"}, @{term "two \<equiv> 2::nat"}
+  and @{term "three \<equiv> 3::nat"}. The point of this code is that we augment the initial
+  context with the definitions. The result we are interested in is the
+  augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing 
+  information about the definitions---the function @{ML_ind add_def in Local_Defs} returns
+  both as pairs. We can use this information for example to print out the definiens and 
+  the theorem corresponding to the definitions. For example for the first definition:
+
+  @{ML_response_fake [display, gray]
+  "let 
+  val (one_trm, one_thm) = one_def
+in
+  pwriteln (pretty_term ctxt' one_trm);
+  pwriteln (pretty_thm ctxt' one_thm)
+end"
+  "one
+one \<equiv> 1"}
+
   Recall that @{ML "|>"} is the reverse function application. Recall also that
   the related reverse function composition is @{ML "#>"}. In fact all the
   combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
@@ -739,13 +739,9 @@
   contains further information about combinators.
   \end{readmore}
 
-  \footnote{\bf FIXME: find a good exercise for combinators}
   \begin{exercise}
   Find out what the combinator @{ML "K I"} does.
   \end{exercise}
-
-
-  \footnote{\bf FIXME: say something about calling conventions} 
 *}
 
 
@@ -901,7 +897,7 @@
   To use it you also have to install it using \isacommand{setup} like so
 *}
 
-setup{* term_pat_setup *}
+setup %gray {* term_pat_setup *}
 
 text {*
   The parser in Line 2 provides us with a context and a string; this string is
@@ -934,7 +930,7 @@
   which can be installed with
 *}
 
-setup{* type_pat_setup *}
+setup %gray {* type_pat_setup *}
 
 text {*
   However, a word of warning is in order: Introducing new antiquotations
@@ -1398,24 +1394,4 @@
   \end{conventions}
 
 *}
-
-
-(**************************************************)
-(* bak                                            *)
-(**************************************************)
-
-(*
-section {* Do Not Try This At Home! *}
-
-ML {* val my_thms = ref ([]: thm list) *}
-
-attribute_setup my_thm_bad =
-  {* Scan.succeed (Thm.declaration_attribute (fn th => fn ctxt =>
-      (my_thms := th :: ! my_thms; ctxt))) *} "bad attribute"
-
-declare sym [my_thm_bad]
-declare refl [my_thm_bad]
-
-ML "!my_thms"
-*)
 end