--- a/ProgTutorial/General.thy	Sun Nov 15 13:18:07 2009 +0100
+++ b/ProgTutorial/General.thy	Sun Nov 15 13:47:31 2009 +0100
@@ -740,20 +740,19 @@
   \begin{figure}[t]
   \begin{minipage}{\textwidth}
   \begin{isabelle}*}
-ML{*fun pretty_helper f env =
+ML{*fun pretty_helper aux env =
   env |> Vartab.dest  
-      |> map f 
+      |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux) 
       |> commas 
       |> enclose "[" "]" 
       |> tracing
 
 fun pretty_tyenv ctxt tyenv =
 let
-  fun aux (v, (s, T)) =
-        Syntax.string_of_typ ctxt (TVar (v, s)) 
-          ^ " := " ^ Syntax.string_of_typ ctxt T
+  fun get_typs (v, (s, T)) = (TVar (v, s), T)
+  val print = pairself (Syntax.string_of_typ ctxt)
 in 
-  pretty_helper aux tyenv
+  pretty_helper (print o get_typs) tyenv
 end*}
 text_raw {*
   \end{isabelle}
@@ -927,14 +926,14 @@
 
 ML{*fun pretty_env ctxt env =
 let
-  fun aux (v, (T, t)) =
-        string_of_term ctxt (Var (v, T)) ^ " := " ^ string_of_term ctxt t
+  fun get_trms (v, (T, t)) = (Var (v, T), t) 
+  val print = pairself (string_of_term ctxt)
 in
-  pretty_helper aux env 
+  pretty_helper (print o get_trms) env 
 end*}
 
 text {*
-  As can be seen from the @{text "aux"}-function, a term environment associates 
+  As can be seen from the @{text "get_trms"}-function, a term environment associates 
   a schematic term variable with a type and a term.  An example of a first-order 
   matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern 
   @{text "?X ?Y"}.

Binary file progtutorial.pdf has changed