# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1243037994 -7200
# Node ID f380b13b25a774e84156feb4551ede85ef1658c6
# Parent  cccb25ee13096cda5d64b322b155c8a4a30ae521
added an example

diff -r cccb25ee1309 -r f380b13b25a7 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon May 18 05:21:40 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat May 23 02:19:54 2009 +0200
@@ -344,7 +344,15 @@
   into a list of variable terms in Line 6, which in the last line is applied
   by the function @{ML list_comb} to the function. In this last step we have to 
   use the function @{ML curry}, because @{ML list_comb} expects the function and the
-  variables list as a pair.
+  variables list as a pair. This kind of functions is often needed when
+  constructing terms and the infrastructure helps tremendously to avoid
+  any name clashes. Consider for example: 
+
+   @{ML_response_fake [display,gray]
+"apply_fresh_args @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"} @{context} 
+ |> Syntax.string_of_term @{context}
+ |> writeln"
+  "za z zb"}
   
   The combinator @{ML "#>"} is the reverse function composition. It can be
   used to define the following function
@@ -997,11 +1005,11 @@
   change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 
-ML{*fun nat_to_int t =
-  (case t of
+ML{*fun nat_to_int ty =
+  (case ty of
      @{typ nat} => @{typ int}
-   | Type (s, ts) => Type (s, map nat_to_int ts)
-   | _ => t)*}
+   | Type (s, tys) => Type (s, map nat_to_int tys)
+   | _ => ty)*}
 
 text {*
   Here is an example:
@@ -1321,7 +1329,7 @@
   context (which we ignore in the code above) and a theorem (@{text thm}), and 
   returns another theorem (namely @{text thm} resolved with the theorem 
   @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained
-  later on in Section~\ref{sec:simpletacs}.} The function 
+  in Section~\ref{sec:simpletacs}.} The function 
   @{ML "Thm.rule_attribute"} then returns 
   an attribute.
 
diff -r cccb25ee1309 -r f380b13b25a7 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Mon May 18 05:21:40 2009 +0200
+++ b/ProgTutorial/Intro.thy	Sat May 23 02:19:54 2009 +0200
@@ -67,7 +67,7 @@
 
 *}
 
-section {* Typographic Conventions in the Tutorial *}
+section {* Typographic Conventions *}
 
 text {*
 
@@ -119,7 +119,7 @@
   to solve the exercises on your own, and then look at the solutions.
 *}
 
-section {* Naming Conventions in the Isabelle Sources *}
+section {* Some Naming Conventions in the Isabelle Sources *}
 
 text {*
   There are a few naming conventions in Isabelle that might aid reading 
diff -r cccb25ee1309 -r f380b13b25a7 progtutorial.pdf
Binary file progtutorial.pdf has changed