# HG changeset patch
# User wenzelm
# Date 1292416550 -3600
# Node ID 2181c47a02fe2523c36345c4234058a5c49162a6
# Parent  988af70bff208fc27f86a985606de4e486919619
more correct ML snippets that are unchecked;
tuned comments;

diff -r 988af70bff20 -r 2181c47a02fe doc-src/IsarImplementation/Thy/ML.thy
--- 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
 *}
diff -r 988af70bff20 -r 2181c47a02fe doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Dec 15 11:59:23 2010 +0000
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Dec 15 13:35:50 2010 +0100
@@ -509,10 +509,16 @@
       val y = ...
     in ... end
 
+
+  (* WRONG *)
+
   fun foo x = let
     val y = ...
   in ... end
 
+
+  (* WRONG *)
+
   fun foo x =
   let
     val y = ...
@@ -1010,7 +1016,7 @@
   \medskip
   \begin{tabular}{lll}
   \isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{f\ x} \\
-  \isa{f\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\ g} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ g} \\
+  \isa{{\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{23}{\isacharhash}}{\isaliteral{3E}{\isachargreater}}\ g{\isaliteral{29}{\isacharparenright}}\ x} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ g} \\
   \end{tabular}
   \medskip
 
@@ -1024,7 +1030,7 @@
   \medskip
   \begin{tabular}{lll}
   \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ f} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{f\ x\ y} \\
-  \isa{f\ {\isaliteral{23}{\isacharhash}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ g} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ g} \\
+  \isa{{\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{23}{\isacharhash}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ g{\isaliteral{29}{\isacharparenright}}\ x} & \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} & \isa{x\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{3E}{\isachargreater}}\ f\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ g} \\
   \end{tabular}
   \medskip%
 \end{isamarkuptext}%