# HG changeset patch
# User haftmann
# Date 1441570492 -7200
# Node ID 774752af4a1ff3de5a9708a0adfad2cbd77ff662
# Parent  8e5072cba671db5690cec783dbab5325dff3cc7a
parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope;
with explicit regression setup

diff -r 8e5072cba671 -r 774752af4a1f src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Sun Sep 06 22:14:52 2015 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Sun Sep 06 22:14:52 2015 +0200
@@ -12,6 +12,8 @@
   "~~/src/HOL/ex/Records"
 begin
 
+text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close>
+
 setup \<open>
 fn thy =>
 let
@@ -19,7 +21,9 @@
   val consts = map_filter (try (curry (Axclass.param_of_inst thy)
     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
 in fold Code.del_eqns consts thy end
-\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
+\<close>
+
+text \<open>Simple example for the predicate compiler.\<close>
 
 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 where
@@ -29,6 +33,26 @@
 
 code_pred sublist .
 
-code_reserved SML upto -- {* avoid popular infix *}
+text \<open>Avoid popular infix.\<close>
+
+code_reserved SML upto
+
+text \<open>Explicit check in @{text OCaml} for correct precedence of let expressions in list expressions\<close>
+
+definition funny_list :: "bool list"
+where
+  "funny_list = [let b = True in b, False]"
+
+definition funny_list' :: "bool list"
+where
+  "funny_list' = funny_list"
+
+lemma [code]:
+  "funny_list' = [True, False]"
+  by (simp add: funny_list_def funny_list'_def)
+
+definition check_list :: unit
+where
+  "check_list = (if funny_list = funny_list' then () else undefined)"
 
 end
diff -r 8e5072cba671 -r 774752af4a1f src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Sep 06 22:14:52 2015 +0200
+++ b/src/Tools/Code/code_ml.ML	Sun Sep 06 22:14:52 2015 +0200
@@ -454,8 +454,7 @@
                   [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map print_let binds vars;
           in
-            brackify_block fxy (Pretty.chunks ps) []
-              (print_term is_pseudo_fun some_thm vars' NOBR body)
+            brackets [Pretty.chunks ps, print_term is_pseudo_fun some_thm vars' NOBR body]
           end
       | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
           let