# HG changeset patch
# User wenzelm
# Date 1236679288 -3600
# Node ID 81218f70997fc80bc67b47c3c51d314a8c18d5fe
# Parent  15dc25f8a0e2bf994cbb00bb6e4ebd498bf89fcf# Parent  bd38973f39e5ddd67351fe665153b92166cc5788
merged

diff -r 15dc25f8a0e2 -r 81218f70997f doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue Mar 10 08:47:45 2009 +0000
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue Mar 10 11:01:28 2009 +0100
@@ -533,11 +533,11 @@
   Likewise, \verb!concl! may be used as a style to show just the
   conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
   \begin{center}
-    \isa{{\isacharparenleft}xs{\isasymColon}{\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+    \isa{{\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   \end{center}
   To print just the conclusion,
   \begin{center}
-    \isa{hd\ {\isacharparenleft}xs{\isasymColon}{\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+    \isa{hd\ {\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   \end{center}
   type
   \begin{quote}
diff -r 15dc25f8a0e2 -r 81218f70997f src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Tue Mar 10 08:47:45 2009 +0000
+++ b/src/HOL/Library/OptionalSugar.thy	Tue Mar 10 11:01:28 2009 +0100
@@ -9,7 +9,7 @@
 
 (* set *)
 translations
-  "xs" <= "set xs"
+  "xs" <= "CONST set xs"
 
 (* append *)
 syntax (latex output)
@@ -26,15 +26,15 @@
 
 (* Let *)
 translations 
-  "_bind (p,DUMMY) e" <= "_bind p (fst e)"
-  "_bind (DUMMY,p) e" <= "_bind p (snd e)"
+  "_bind (p,DUMMY) e" <= "_bind p (CONST fst e)"
+  "_bind (DUMMY,p) e" <= "_bind p (CONST snd e)"
 
   "_tuple_args x (_tuple_args y z)" ==
     "_tuple_args x (_tuple_arg (_tuple y z))"
 
-  "_bind (Some p) e" <= "_bind p (the e)"
-  "_bind (p#DUMMY) e" <= "_bind p (hd e)"
-  "_bind (DUMMY#p) e" <= "_bind p (tl e)"
+  "_bind (Some p) e" <= "_bind p (CONST the e)"
+  "_bind (p#DUMMY) e" <= "_bind p (CONST hd e)"
+  "_bind (DUMMY#p) e" <= "_bind p (CONST tl e)"
 
 (* type constraints with spacing *)
 setup {*