# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1327159118 0
# Node ID 633d3f013be2c2f0e2a4c0bf3c1eb970c749fcc4
# Parent  d770a7b31aeb00ef208117296a98eb20b6a118d8# Parent  caa7331904544bbafb49da779a7089f6d212b1ea
merged

diff -r caa733190454 -r 633d3f013be2 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Mon Jan 16 07:40:17 2012 +0000
+++ b/ProgTutorial/Essential.thy	Sat Jan 21 15:18:38 2012 +0000
@@ -87,17 +87,23 @@
   with beta-redexes
 
   @{ML_response_fake [display, gray]
-"@{term \"(\<lambda>x y. x) 1 2\"}
+"@{term \"(\<lambda>(x::int) (y::int). x)\"} $ @{term \"1::int\"} $ @{term \"2::int\"}
   |> pretty_term @{context}
   |> pwriteln"
   "1"}
 
-  There is a configuration value to switch off the tacit eta-contraction (see
-  \ref{sec:printing}), but none for beta-contraction. So in certain cases you
-  might have to inspect the internal representation of a term, instead of
-  pretty printing it. Because of the alluded puzzlement that might arise from
-  this feature of Isabelle, it is certainly an acrane fact that you should
-  keep in mind about pretty-printing terms.
+  There is a dedicated configuration value for switching off the tacit
+  eta-contraction, namely @{ML_ind eta_contract in Syntax} (see Section
+  \ref{sec:printing}), but none for beta-contractions. However you can avoid
+  the beta-contractions by switching off abbreviation using the configuration
+  value @{ML_ind show_abbrevs in Syntax}. For example
+
+
+  @{ML_response_fake [display, gray]
+  "@{term \"(\<lambda>(x::int) (y::int). x)\"} $ @{term \"1::int\"} $ @{term \"2::int\"}
+  |> pretty_term (Config.put show_abbrevs false @{context})
+  |> pwriteln"
+  "(\<lambda>x y. x) 1 2"}
 
   Isabelle makes a distinction between \emph{free} variables (term-constructor
   @{ML Free} and written on the user level in blue colour) and
diff -r caa733190454 -r 633d3f013be2 progtutorial.pdf
Binary file progtutorial.pdf has changed