--- a/ProgTutorial/First_Steps.thy	Tue Jun 14 22:09:40 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Fri Jun 17 16:58:05 2011 +0100
@@ -57,7 +57,8 @@
   \end{graybox}
   \end{isabelle}
 
-  Like normal Isabelle scripts, \isacommand{ML}-commands can be evaluated by
+  If you work with ProofGeneral then like normal Isabelle scripts 
+  \isacommand{ML}-commands can be evaluated by
   using the advance and undo buttons of your Isabelle environment. The code
   inside the \isacommand{ML}-command can also contain value and function
   bindings, for example
@@ -148,18 +149,10 @@
   @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 
 
   However, @{text "@{makes_tring}"} only works if the type of what
-  is converted is monomorphic and not a function.
+  is converted is monomorphic and not a function. 
 
-  The function @{ML "writeln"} should only be used for testing purposes,
-  because any output this function generates will be overwritten as soon as an
-  error is raised. For printing anything more serious and elaborate, the
-  function @{ML_ind tracing in Output} is more appropriate. This function writes all
-  output into a separate tracing buffer. For example:
-
-  @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
-
-  You can print out error messages with the function @{ML_ind error in Library}; for 
-  example:
+  You can print out error messages with the function @{ML_ind error in Library}; 
+  for example:
 
   @{ML_response_fake [display,gray] 
   "if 0=1 then true else (error \"foo\")" 
@@ -168,40 +161,13 @@
 
   This function raises the exception @{text ERROR}, which will then 
   be displayed by the infrastructure. Note that this exception is meant 
-  for ``user-level'' error messages seen by the ``end-user''.
-
+  for ``user-level'' error messages seen by the ``end-user''. 
+  
   For messages where you want to indicate a genuine program error, then
   use the exception @{text Fail}. Here the infrastructure indicates that this 
   is a low-level exception, and also prints the source position of the ML 
   raise statement. 
 
-
-  \footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and 
-  @{ML_ind profiling in Toplevel}.}
-
-*}
-
-(* FIXME*)
-(*
-ML {* reset Toplevel.debug *}
-
-ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}
-
-ML {* fun innocent () = dodgy_fun () *}
-ML {* exception_trace (fn () => cterm_of @{theory} (Bound 0)) *}
-ML {* exception_trace (fn () => innocent ()) *}
-
-ML {* Toplevel.program (fn () => cterm_of @{theory} (Bound 0)) *}
-
-ML {* Toplevel.program (fn () => innocent ()) *}
-*)
-
-text {*
-  %Kernel exceptions TYPE, TERM, THM also have their place in situations 
-  %where kernel-like operations are involved.  The printing is similar as for 
-  %Fail, although there is some special treatment when Toplevel.debug is 
-  %enabled.
-
   Most often you want to inspect data of Isabelle's basic data structures,
   namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
   and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
@@ -252,13 +218,17 @@
 
 text {*
   @{ML_response_fake [display, gray]
-  "pwriteln (pretty_term 
-  (Config.put show_all_types true @{context}) @{term \"(1::nat, x)\"})"
+  "let 
+  val show_all_types_ctxt = Config.put show_all_types true @{context}
+in
+  pwriteln (pretty_term show_all_types_ctxt @{term \"(1::nat, x)\"})
+end"
   "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
 
-  where @{term Pair} is the term-constructor for products. 
-  Other configuration values that influence printing of terms are 
-  @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}. 
+  where now even @{term Pair} is written with its type (@{term Pair} is the
+  term-constructor for products). Other configuration values that influence
+  printing of terms are @{ML_ind show_brackets in Syntax} and @{ML_ind
+  show_sorts in Syntax}.
 *}
 
 text {*
@@ -297,21 +267,15 @@
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
   However, in order to improve the readability when printing theorems, we
-  convert these schematic variables into free variables using the function
-  @{ML_ind  import in Variable}. This is similar to statements like @{text
-  "conjI[no_vars]"} on Isabelle's user-level.
+  can switch off the question marks as follows:
 *}
 
-ML{*fun no_vars ctxt thm =
-let 
-  val ((_, [thm']), _) = Variable.import true [thm] ctxt
+ML{*fun pretty_thm_no_vars ctxt thm =
+let
+  val ctxt' = Config.put show_question_marks false ctxt
 in
-  thm'
-end
-
-fun pretty_thm_no_vars ctxt thm =
-  pretty_term ctxt (prop_of (no_vars ctxt thm))*}
-
+  pretty_term ctxt' (prop_of thm)
+end*}
 
 text {* 
   With this function, theorem @{thm [source] conjI} is now printed as follows:
@@ -542,12 +506,12 @@
   The remaining combinators we describe in this section add convenience for the
   ``waterfall method'' of writing functions. The combinator @{ML_ind tap in
   Basics} allows you to get hold of an intermediate result (to do some
-  side-calculations for instance). The function
+  side-calculations or print out an intermediate result, for instance). The function
  *}
 
 ML %linenosgray{*fun inc_by_three x =
      x |> (fn x => x + 1)
-       |> tap (fn x => tracing (PolyML.makestring x))
+       |> tap (fn x => writeln (@{make_string} x))
        |> (fn x => x + 2)*}
 
 text {*