doc-src/IsarImplementation/Thy/ML.thy
changeset 41162 2181c47a02fe
parent 40964 482a8334ee9e
child 42510 b9c106763325
--- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Dec 15 11:59:23 2010 +0000
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Dec 15 13:35:50 2010 +0100
@@ -488,10 +488,16 @@
       val y = ...
     in ... end
 
+
+  (* WRONG *)
+
   fun foo x = let
     val y = ...
   in ... end
 
+
+  (* WRONG *)
+
   fun foo x =
   let
     val y = ...
@@ -825,7 +831,7 @@
   \medskip
   \begin{tabular}{lll}
   @{text "x |> f"} & @{text "\<equiv>"} & @{text "f x"} \\
-  @{text "f #> g"} & @{text "\<equiv>"} & @{text "x |> f |> g"} \\
+  @{text "(f #> g) x"} & @{text "\<equiv>"} & @{text "x |> f |> g"} \\
   \end{tabular}
   \medskip
 
@@ -840,7 +846,7 @@
   \medskip
   \begin{tabular}{lll}
   @{text "(x, y) |-> f"} & @{text "\<equiv>"} & @{text "f x y"} \\
-  @{text "f #-> g"} & @{text "\<equiv>"} & @{text "x |> f |-> g"} \\
+  @{text "(f #-> g) x"} & @{text "\<equiv>"} & @{text "x |> f |-> g"} \\
   \end{tabular}
   \medskip
 *}